forked from hoelzl/Snark
-
Notifications
You must be signed in to change notification settings - Fork 1
Mark Stickel's Snark theorem prover
License
alanruttenberg/Snark
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
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 0
No packages published
Languages
- Common Lisp 87.1%
- TeX 12.8%
- Shell 0.1%