Snark

INSTALL

@@ -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.

README

@@ -0,0 +1,36 @@
+(replace "yyyymmdd" by the SNARK version date)
+
+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.

commons.lisp

@@ -0,0 +1,5 @@
+
+(in-package :snark-user)
+
+(assert-add-table *arithmetic-max*)
+(assert-domain *horizon*)

compile

@@ -0,0 +1,4 @@
+(load "snark-system.lisp")
+(make-snark-system t)
+(make-snark-system :optimize)
+(quit)

examples/BOO002-1+rm_eq_rstfp.kif

@@ -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))
+
+;--------------------------------------------------------------------------

examples/COL003-1+rm_eq_rstfp.kif

@@ -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)))))
+
+;--------------------------------------------------------------------------

examples/COL049-1+rm_eq_rstfp.kif

@@ -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)))))
+
+;--------------------------------------------------------------------------

examples/GRP001-1+rm_eq_rstfp.kif

@@ -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)))
+
+;--------------------------------------------------------------------------