forked from hoelzl/Snark
-
Notifications
You must be signed in to change notification settings - Fork 1
/
README
50 lines (33 loc) · 1.24 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
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