Add working example of LFSC proof with quantifiers. Update quantifiers signature...

diff --git a/proofs/signatures/example-quant.plf b/proofs/signatures/example-quant.plf
new file mode 100755 (executable)
index 0000000..086633b
--- /dev/null
+++ b/proofs/signatures/example-quant.plf
@@ -0,0 +1,95 @@
+; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf
+
+; --------------------------------------------------------------------------------
+; literals :
+; L1 : forall x. x != x
+; L2 : t = t
+
+; input :
+; L1
+
+; (instantiation) lemma : 
+; L1 => L2
+
+; theory conflicts :
+; ~L2
+
+
+;  With the theory lemma, the input is unsatisfiable.
+; --------------------------------------------------------------------------------
+
+
+; (0) -------------------- term declarations -----------------------------------
+
+(check
+(% s sort
+(% t (term s)
+
+
+; (1) -------------------- input formula -----------------------------------
+
+(% x (term s)
+(% A1 (th_holds (forall _ x (not (= _ x x))))
+
+
+
+; (2) ------------------- specify that the following is a proof of the empty clause -----------------
+
+(: (holds cln)
+
+
+
+; (3) -------------------- theory lemmas prior to rewriting/preprocess/CNF -----------------
+;     ---  these should introduce (th_holds ...)
+
+
+; instantiation lemma
+(inst _ _ _ t (not (= _ t t)) A1 (\ A2
+
+
+
+
+; (4) -------------------- map theory literals to boolean variables
+;     --- maps all theory literals involved in proof to boolean literals
+
+(decl_atom (forall _ x (not (= _ x x))) (\ v1 (\ a1
+(decl_atom (= _ t t) (\ v2 (\ a2
+
+
+
+
+; (5) -------------------- theory conflicts ---------------------------------------------
+;     ---  these should introduce (holds ...)
+
+(satlem _ _
+(asf _ _ _ a2 (\ l2
+(clausify_false
+
+   (contra _ (refl _ t) l2)
+   
+))) (\ CT1
+; CT1 is the clause ( v2 )
+
+
+; (6) -------------------- clausification -----------------------------------------
+;     ---  these should introduce (holds ...)
+
+(satlem _ _
+(ast _ _ _ a2 (\ l2
+(clausify_false
+
+  (contra _ l2 A2)
+
+))) (\ C1
+; C1 is the clause ( ~v2 )
+
+
+; (7) -------------------- resolution proof ------------------------------------------------------------
+
+(satlem_simplify _ _ _
+
+(R _ _ CT1 C1 v2)
+
+(\ x x))
+
+))))))))))))))))))

diff --git a/proofs/signatures/th_quant.plf b/proofs/signatures/th_quant.plf
index d1881238063e736cc8eb06b5635c8aeca6831683..98b53e43d21e6439091113c5fbb935e9202a3d3d 100755 (executable)
--- a/proofs/signatures/th_quant.plf
+++ b/proofs/signatures/th_quant.plf
@@ -3,39 +3,69 @@
                 (! f formula\r
                   formula))))\r
 \r
-(program instantiate ((f formula) (t term) (k term))\r
-  (do (markvar t) \r
-     (let f1 (inst_f f t)\r
-        (do (markvar t) f1))))\r
+(program eqterm ((n1 term) (n2 term)) bool\r
+    (do (markvar n1)\r
+        (let s (ifmarked n2 tt ff)\r
+           (do (markvar n1) s))))\r
 \r
-(program instantiate_f ((f formula) (k term)) formula\r
-  (match f \r
-    ((and f1 f2) (and (instantiate_f f1 t) (instantiate_f f2 t)))\r
-    ((or f1 f2) (or (instantiate_f f1 t) (instantiate_f f2 t)))\r
-    ((impl f1 f2) (impl (instantiate_f f1 t) (instantiate_f f2 t)))\r
-    ((not f1) (not (instantiate_f f1 t)))\r
-    ((iff f1 f2) (iff (instantiate_f f1 t) (instantiate_f f2 t)))\r
-    ((xor f1 f2) (xor (instantiate_f f1 t) (instantiate_f f2 t)))\r
-    ((ifte f1 f2 f3) (ifte (instantiate_f f1 t) (instantiate_f f2 t) (instantiate_f f3 t)))\r
-    ((= s t1 t2) (= s (inst_t t1 t) (inst_t t2 t)))\r
-    ((forall t1 f1) (forall t1 (instantiate_f f1 t)))\r
-    (default f)))\r
-\r
-(program instantiate_t ((t term) (k term)) formula\r
+(program is_inst_t ((ti term) (t term) (k term)) bool\r
   (match t\r
-    ((apply s1 s2 t1 t2) (apply s1 s2 t1 (instantiate_t t2 t)))\r
-    (default (ifmarked t k t))))\r
+    ((apply s1 s2 t1 t2) \r
+      (match ti\r
+        ((apply si1 si2 ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))\r
+        (default ff)))\r
+    (default \r
+      (match ti\r
+        ((apply si1 si2 ti1 ti2) ff)\r
+        (default (eqterm ti (ifmarked t k t)))))))\r
+\r
+(program is_inst_f ((fi formula) (f formula) (k term)) bool\r
+  (match f \r
+    ((and f1 f2) (match fi\r
+                  ((and fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))\r
+                  (default ff)))\r
+    ((or f1 f2) (match fi\r
+                  ((or fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))\r
+                  (default ff)))\r
+    ((impl f1 f2) (match fi\r
+                  ((impl fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))\r
+                  (default ff)))\r
+    ((not f1) (match fi\r
+                  ((not fi1) (is_inst_f fi1 f1 k))\r
+                  (default ff)))\r
+    ((iff f1 f2) (match fi\r
+                  ((iff fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))\r
+                  (default ff)))\r
+    ((xor f1 f2) (match fi\r
+                  ((xor fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))\r
+                  (default ff)))\r
+    ((ifte f1 f2 f3) (match fi\r
+                      ((ifte fi1 fi2 fi3) (match (is_inst_f fi1 f1 k) \r
+                                            (tt (match (is_inst_f fi2 f2 k) (tt (is_inst_f fi3 f3 k)) (ff ff))) \r
+                                            (ff ff)))\r
+                      (default ff)))\r
+    ((= s t1 t2) (match fi\r
+                  ((= s ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))\r
+                  (default ff)))\r
+    ((forall s t1 f1) (match fi\r
+                     ((forall s ti1 fi1) (is_inst_f fi1 f1 k))\r
+                     (default ff)))\r
+    (default ff)))\r
 \r
+(program is_inst ((fi formula) (f formula) (t term) (k term)) bool\r
+  (do (markvar t) \r
+     (let f1 (is_inst_f fi f k)\r
+        (do (markvar t) f1))))\r
 \r
 (declare skolem\r
   (! s sort\r
   (! t (term s)\r
   (! f formula\r
   (! p (th_holds (not (forall s t f)))\r
-  (! u (! f1 formula\r
-       (! k (term s)\r
-       (! r (^ (instantiate f t k) f1)\r
-       (! p1 (th_holds (not f1))\r
+  (! u (! k (term s)\r
+       (! fi formula\r
+       (! p1 (th_holds (not fi))\r
+       (! r (^ (is_inst fi f t k) tt)\r
          (holds cln)))))\r
     (holds cln)))))))\r
     \r
@@ -43,10 +73,10 @@
   (! s sort\r
   (! t (term s)\r
   (! f formula\r
-  (! f1 formula\r
-  (! p (th_holds (forall s t f))\r
   (! k (term s)\r
-  (! r (^ (instantiate f t k) f1)\r
-  (! u (! p1 (th_holds f1)\r
+  (! fi formula\r
+  (! p (th_holds (forall s t f))\r
+  (! r (^ (is_inst fi f t k) tt)\r
+  (! u (! p1 (th_holds fi)\r
             (holds cln))\r
     (holds cln))))))))))
\ No newline at end of file