-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
kfp
committed
Feb 25, 2016
0 parents
commit ec86d23
Showing
155 changed files
with
36,843 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,53 @@ | ||
SNARK is run regularly in | ||
Macintosh Common Lisp on Mac OS X | ||
Steel Bank Common Lisp (SBCL) on Mac OS X | ||
Clozure Common Lisp (CCL nee OpenMCL) on Mac OS X | ||
and has been run in other ANSI Common Lisp systems | ||
|
||
After editing for the correct name and location of the SBCL Lisp system in the appropriate make-xxx file | ||
a 32-bit executable of SNARK in SBCL named snark can be made by ./make-snark-sbcl; | ||
a 64-bit executable of SNARK in SBCL named snark64 can be make by ./make-snark-sbcl64. | ||
|
||
After editing for the correct name and location of the CCL Lisp system in the appropriate make-xxx file | ||
a 32-bit executable of SNARK in CCL named snark-ccl can be made by ./make-snark-ccl; | ||
a 64-bit executable of SNARK in CCL named snark-ccl64 can be maded by ./make-snark-ccl64 | ||
|
||
|
||
|
||
Older detailed instructions: | ||
|
||
(replace "yyyymmdd" by the SNARK version date) | ||
|
||
Installing SNARK: | ||
|
||
tar xfz snark-yyyymmdd.tar.gz | ||
cd snark-yyyymmdd | ||
lisp | ||
(load "snark-system.lisp") | ||
(make-snark-system t) ;t specifies compilation | ||
(make-snark-system t) ;compile again for more inlining (optional) | ||
;can use :optimize instead of t to compile for | ||
;higher speed at the expense of less error checking | ||
(quit) | ||
|
||
Running SNARK: | ||
|
||
lisp | ||
(load "snark-system.lisp") | ||
(make-snark-system) ;loads SNARK files compiled above | ||
: | ||
|
||
The lengthy load process in running SNARK can be eliminated | ||
for CCL, SBCL, CMUCL, Allegro Common Lisp, or CLISP by doing | ||
lisp | ||
(load "snark-system.lisp") | ||
(make-snark-system) | ||
(save-snark-system) | ||
after installing SNARK as above. | ||
(save-snark-system) will print instructions for running | ||
the resulting Lisp core image with SNARK preloaded. | ||
|
||
In the case of SBCL, (save-snark-system) can be replaced by | ||
(save-snark-system :name "snark" :executable t) | ||
to create a standalone SNARK executable. This is done | ||
by the make-snark-sbcl and make-snark-sbcl64 scripts. |
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,95 @@ | ||
===== | ||
SNARK | ||
===== | ||
|
||
SNARK, SRI's New Automated Reasoning Kit, is a theorem prover intended for | ||
applications in artificial intelligence and software engineering. SNARK is | ||
geared toward dealing with large sets of assertions; it can be specialized | ||
with strategic controls that tune its performance; and it has facilities | ||
for integrating special-purpose reasoning procedures with general-purpose | ||
inference. | ||
|
||
|
||
-------- | ||
Overview | ||
-------- | ||
|
||
SNARK is an automated theorem-proving program being developed in Common Lisp. | ||
Its principal inference rules are resolution and paramodulation. SNARK's style | ||
of theorem proving is similar to Otter's. | ||
|
||
Some distinctive features of SNARK are its support for special unification | ||
algorithms, sorts, answer construction for program synthesis, procedural | ||
attachment, and extensibility by Lisp code. | ||
|
||
SNARK has been used as the reasoning component of SRI's High Performance | ||
Knowledge Base (HPKB) system, which deduces answers to questions based on | ||
large repositories of information, and as the deductive core of NASA's Amphion | ||
system, which composes software from components to meet users' specifications, | ||
e.g., to perform computations in planetary astronomy. SNARK has also been | ||
connected to Kestrel's SPECWARE environment for software development. | ||
|
||
|
||
Selected Publications | ||
|
||
Stickel, M., R. Waldinger, M. Lowry, T. Pressburger, and I. Underwood. | ||
Deductive composition of astronomical software from subroutine libraries. | ||
Proceedings of the Twelfth International Conference on Automated Deduction | ||
(CADE-12), Nancy, France, June 1994, 341-355. | ||
|
||
|
||
--------------------- | ||
Links & Documentation | ||
--------------------- | ||
|
||
SNARK tutorial ... http://www.ai.sri.com/snark/tutorial/tutorial.html | ||
SNARK paper ...... http://www.sri.com/work/publications/guide-snark | ||
SNARK home ....... http://www.ai.sri.com/~stickel/snark.html | ||
SNARK author ..... https://en.wikipedia.org/wiki/Mark_E._Stickel | ||
|
||
|
||
---------------- | ||
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) | ||
: | ||
|
||
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. | ||
|
||
----- | ||
NOTES | ||
----- | ||
This repository is based on the latest version 20120808-r022 from the | ||
download site and the '.asd' files from https://github.com/hoelzl/Snark. | ||
The goal is to get SNARK installable by QuickLisp. | ||
|
||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,4 @@ | ||
(load "snark-system.lisp") | ||
(make-snark-system t) | ||
(make-snark-system :optimize) | ||
(quit) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,47 @@ | ||
;-------------------------------------------------------------------------- | ||
; File : BOO002-1 : TPTP v2.2.0. Released v1.0.0. | ||
; Domain : Boolean Algebra (Ternary) | ||
; Problem : In B3 algebra, X * X^-1 * Y = Y | ||
; Version : [OTTER] (equality) axioms : Reduced > Incomplete. | ||
; English : | ||
|
||
; Refs : [LO85] Lusk & Overbeek (1985), Reasoning about Equality | ||
; : [Ove90] Overbeek (1990), ATP competition announced at CADE-10 | ||
; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal | ||
; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11 | ||
; : [Zha93] Zhang (1993), Automated Proofs of Equality Problems in | ||
; Source : [Ove90] | ||
; Names : Problem 5 [LO85] | ||
; : CADE-11 Competition Eq-3 [Ove90] | ||
; : THEOREM EQ-3 [LM93] | ||
; : PROBLEM 3 [Zha93] | ||
|
||
; Status : unsatisfiable | ||
; Rating : 0.33 v2.2.0, 0.43 v2.1.0, 0.38 v2.0.0 | ||
; Syntax : Number of clauses : 5 ( 0 non-Horn; 5 unit; 1 RR) | ||
; Number of literals : 5 ( 5 equality) | ||
; Maximal clause size : 1 ( 1 average) | ||
; Number of predicates : 1 ( 0 propositional; 2-2 arity) | ||
; Number of functors : 4 ( 2 constant; 0-3 arity) | ||
; Number of variables : 11 ( 2 singleton) | ||
; Maximal term depth : 3 ( 2 average) | ||
|
||
; Comments : | ||
; : tptp2X -f kif -t rm_equality:rstfp BOO002-1.p | ||
;-------------------------------------------------------------------------- | ||
; associativity, axiom. | ||
(or (= (multiply (multiply ?A ?B ?C) ?D (multiply ?A ?B ?E)) (multiply ?A ?B (multiply ?C ?D ?E)))) | ||
|
||
; ternary_multiply_1, axiom. | ||
(or (= (multiply ?A ?B ?B) ?B)) | ||
|
||
; ternary_multiply_2, axiom. | ||
(or (= (multiply ?A ?A ?B) ?A)) | ||
|
||
; left_inverse, axiom. | ||
(or (= (multiply (inverse ?A) ?A ?B) ?B)) | ||
|
||
; prove_equation, conjecture. | ||
(or (/= (multiply a (inverse a) b) b)) | ||
|
||
;-------------------------------------------------------------------------- |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,53 @@ | ||
;-------------------------------------------------------------------------- | ||
; File : COL003-1 : TPTP v2.2.0. Released v1.0.0. | ||
; Domain : Combinatory Logic | ||
; Problem : Strong fixed point for B and W | ||
; Version : [WM88] (equality) axioms. | ||
; English : The strong fixed point property holds for the set | ||
; P consisting of the combinators B and W alone, where ((Bx)y)z | ||
; = x(yz) and (Wx)y = (xy)y. | ||
|
||
; Refs : [Smu85] Smullyan (1978), To Mock a Mocking Bird and Other Logi | ||
; : [MW87] McCune & Wos (1987), A Case Study in Automated Theorem | ||
; : [WM88] Wos & McCune (1988), Challenge Problems Focusing on Eq | ||
; : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr | ||
; : [Ove90] Overbeek (1990), ATP competition announced at CADE-10 | ||
; : [LW92] Lusk & Wos (1992), Benchmark Problems in Which Equalit | ||
; : [Wos93] Wos (1993), The Kernel Strategy and Its Use for the St | ||
; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal | ||
; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11 | ||
; : [Zha93] Zhang (1993), Automated Proofs of Equality Problems in | ||
; Source : [WM88] | ||
; Names : C2 [WM88] | ||
; : Test Problem 17 [Wos88] | ||
; : Sages and Combinatory Logic [Wos88] | ||
; : CADE-11 Competition Eq-8 [Ove90] | ||
; : CL2 [LW92] | ||
; : THEOREM EQ-8 [LM93] | ||
; : Question 3 [Wos93] | ||
; : Question 5 [Wos93] | ||
; : PROBLEM 8 [Zha93] | ||
|
||
; Status : unknown | ||
; Rating : 1.00 v2.0.0 | ||
; Syntax : Number of clauses : 3 ( 0 non-Horn; 3 unit; 1 RR) | ||
; Number of literals : 3 ( 3 equality) | ||
; Maximal clause size : 1 ( 1 average) | ||
; Number of predicates : 1 ( 0 propositional; 2-2 arity) | ||
; Number of functors : 4 ( 2 constant; 0-2 arity) | ||
; Number of variables : 6 ( 0 singleton) | ||
; Maximal term depth : 4 ( 3 average) | ||
|
||
; Comments : | ||
; : tptp2X -f kif -t rm_equality:rstfp COL003-1.p | ||
;-------------------------------------------------------------------------- | ||
; b_definition, axiom. | ||
(or (= (apply (apply (apply b ?A) ?B) ?C) (apply ?A (apply ?B ?C)))) | ||
|
||
; w_definition, axiom. | ||
(or (= (apply (apply w ?A) ?B) (apply (apply ?A ?B) ?B))) | ||
|
||
; prove_strong_fixed_point, conjecture. | ||
(or (/= (apply ?A (f ?A)) (apply (f ?A) (apply ?A (f ?A))))) | ||
|
||
;-------------------------------------------------------------------------- |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,52 @@ | ||
;-------------------------------------------------------------------------- | ||
; File : COL049-1 : TPTP v2.2.0. Released v1.0.0. | ||
; Domain : Combinatory Logic | ||
; Problem : Strong fixed point for B, W, and M | ||
; Version : [WM88] (equality) axioms. | ||
; English : The strong fixed point property holds for the set | ||
; P consisting of the combinators B, W, and M, where ((Bx)y)z | ||
; = x(yz), (Wx)y = (xy)y, Mx = xx. | ||
|
||
; Refs : [Smu85] Smullyan (1978), To Mock a Mocking Bird and Other Logi | ||
; : [MW87] McCune & Wos (1987), A Case Study in Automated Theorem | ||
; : [WM88] Wos & McCune (1988), Challenge Problems Focusing on Eq | ||
; : [Ove90] Overbeek (1990), ATP competition announced at CADE-10 | ||
; : [LW92] Lusk & Wos (1992), Benchmark Problems in Which Equalit | ||
; : [Wos93] Wos (1993), The Kernel Strategy and Its Use for the St | ||
; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal | ||
; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11 | ||
; : [Zha93] Zhang (1993), Automated Proofs of Equality Problems in | ||
; Source : [Ove90] | ||
; Names : Problem 2 [WM88] | ||
; : CADE-11 Competition Eq-6 [Ove90] | ||
; : CL1 [LW92] | ||
; : THEOREM EQ-6 [LM93] | ||
; : Question 2 [Wos93] | ||
; : PROBLEM 6 [Zha93] | ||
|
||
; Status : unsatisfiable | ||
; Rating : 0.22 v2.2.0, 0.14 v2.1.0, 0.62 v2.0.0 | ||
; Syntax : Number of clauses : 4 ( 0 non-Horn; 4 unit; 1 RR) | ||
; Number of literals : 4 ( 4 equality) | ||
; Maximal clause size : 1 ( 1 average) | ||
; Number of predicates : 1 ( 0 propositional; 2-2 arity) | ||
; Number of functors : 5 ( 3 constant; 0-2 arity) | ||
; Number of variables : 7 ( 0 singleton) | ||
; Maximal term depth : 4 ( 3 average) | ||
|
||
; Comments : | ||
; : tptp2X -f kif -t rm_equality:rstfp COL049-1.p | ||
;-------------------------------------------------------------------------- | ||
; b_definition, axiom. | ||
(or (= (apply (apply (apply b ?A) ?B) ?C) (apply ?A (apply ?B ?C)))) | ||
|
||
; w_definition, axiom. | ||
(or (= (apply (apply w ?A) ?B) (apply (apply ?A ?B) ?B))) | ||
|
||
; m_definition, axiom. | ||
(or (= (apply m ?A) (apply ?A ?A))) | ||
|
||
; prove_strong_fixed_point, conjecture. | ||
(or (/= (apply ?A (f ?A)) (apply (f ?A) (apply ?A (f ?A))))) | ||
|
||
;-------------------------------------------------------------------------- |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,78 @@ | ||
;-------------------------------------------------------------------------- | ||
; File : GRP001-1 : TPTP v2.2.0. Released v1.0.0. | ||
; Domain : Group Theory | ||
; Problem : X^2 = identity => commutativity | ||
; Version : [MOW76] axioms. | ||
; English : If the square of every element is the identity, the system | ||
; is commutative. | ||
|
||
; Refs : [Rob63] Robinson (1963), Theorem Proving on the Computer | ||
; : [Wos65] Wos (1965), Unpublished Note | ||
; : [MOW76] McCharen et al. (1976), Problems and Experiments for a | ||
; : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S | ||
; : [Ove90] Overbeek (1990), ATP competition announced at CADE-10 | ||
; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal | ||
; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11 | ||
; Source : [MOW76] | ||
; Names : - [Rob63] | ||
; : wos10 [WM76] | ||
; : G1 [MOW76] | ||
; : CADE-11 Competition 1 [Ove90] | ||
; : THEOREM 1 [LM93] | ||
; : xsquared.ver1.in [ANL] | ||
|
||
; Status : unsatisfiable | ||
; Rating : 0.00 v2.0.0 | ||
; Syntax : Number of clauses : 11 ( 0 non-Horn; 8 unit; 5 RR) | ||
; Number of literals : 19 ( 1 equality) | ||
; Maximal clause size : 4 ( 1 average) | ||
; Number of predicates : 2 ( 0 propositional; 2-3 arity) | ||
; Number of functors : 6 ( 4 constant; 0-2 arity) | ||
; Number of variables : 23 ( 0 singleton) | ||
; Maximal term depth : 2 ( 1 average) | ||
|
||
; Comments : | ||
; : tptp2X -f kif -t rm_equality:rstfp GRP001-1.p | ||
;-------------------------------------------------------------------------- | ||
; left_identity, axiom. | ||
(or (product identity ?A ?A)) | ||
|
||
; right_identity, axiom. | ||
(or (product ?A identity ?A)) | ||
|
||
; left_inverse, axiom. | ||
(or (product (inverse ?A) ?A identity)) | ||
|
||
; right_inverse, axiom. | ||
(or (product ?A (inverse ?A) identity)) | ||
|
||
; total_function1, axiom. | ||
(or (product ?A ?B (multiply ?A ?B))) | ||
|
||
; total_function2, axiom. | ||
(or (not (product ?A ?B ?C)) | ||
(not (product ?A ?B ?D)) | ||
(= ?C ?D)) | ||
|
||
; associativity1, axiom. | ||
(or (not (product ?A ?B ?C)) | ||
(not (product ?B ?D ?E)) | ||
(not (product ?C ?D ?F)) | ||
(product ?A ?E ?F)) | ||
|
||
; associativity2, axiom. | ||
(or (not (product ?A ?B ?C)) | ||
(not (product ?B ?D ?E)) | ||
(not (product ?A ?E ?F)) | ||
(product ?C ?D ?F)) | ||
|
||
; square_element, hypothesis. | ||
(or (product ?A ?A identity)) | ||
|
||
; a_times_b_is_c, hypothesis. | ||
(or (product a b c)) | ||
|
||
; prove_b_times_a_is_c, conjecture. | ||
(or (not (product b a c))) | ||
|
||
;-------------------------------------------------------------------------- |
Oops, something went wrong.