Skip to content

alanruttenberg/Snark

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

10 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Obtaining SNARK:

  SNARK can be downloaded from the SNARK web page
  http://www.ai.sri.com/~stickel/snark.html

See INSTALL file for installation instructions

Running SNARK:

  lisp
  (load "snark-system.lisp")
  (make-snark-system)
  :

OR

(asdf::oos 'asdf::load-op 'snark)

Examples:

  (overbeek-test) in overbeek-test.lisp
    some standard theorem-proving examples, some time-consuming

  (steamroller-example) in steamroller-example.lisp
    illustrates sorts

  (front-last-example) in front-last-example.lisp
    illustrates program synthesis

  (reverse-example) in reverse-example.lisp
    illustrates logic programming style usage

A guide to SNARK has been written:

  http://www.ai.sri.com/snark/tutorial/tutorial.html

but has not been updated yet to reflect changes in SNARK,
especially for temporal and spatial reasoning.

Some other documentation issues noticed:

 - The documentation for sorts is out of sync.
  - declare-disjoint-sorts -> declare-sorts-incompatible
  - declare-subsorts -> declare-subsort (do them one at a time)
  - declare-sort-partition -> ??
  - declare-function-symbol -> declare-function
  - declare-predicate-symbol -> declare-relation
  - declare-variable-symbol -> declare-variable

Please submit an issue if you find others

About

Mark Stickel's Snark theorem prover

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Common Lisp 87.1%
  • TeX 12.8%
  • Shell 0.1%