Adding example proof signatures for LFSC.

1 files changed, 313 insertions, 0 deletions

diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf
new file mode 100755
index 000000000..75bfc442f
--- /dev/null
+++ b/proofs/signatures/smt.plf
@@ -0,0 +1,313 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; SMT syntax and semantics (not theory-specific)
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(declare formula type)
+(declare th_holds (! f formula type))
+
+; constants
+(declare true formula)
+(declare false formula)
+
+; logical connectives
+(declare not (! f formula formula))
+(declare and (! f1 formula (! f2 formula formula)))
+(declare or (! f1 formula (! f2 formula formula)))
+(declare impl (! f1 formula (! f2 formula formula)))
+(declare iff (! f1 formula (! f2 formula formula)))
+(declare xor (! f1 formula (! f2 formula formula)))
+(declare ifte (! b formula (! f1 formula (! f2 formula formula))))
+
+; terms
+(declare sort type)				; sort in the theory
+(declare arrow (! s1 sort (! s2 sort sort)))	; function constructor
+
+(declare term (! t sort type))	; declared terms in formula
+
+(declare apply (! s1 sort
+               (! s2 sort
+               (! t1 (term (arrow s1 s2))
+               (! t2 (term s1)
+                (term s2))))))
+                
+(declare ite (! s sort
+             (! f formula
+             (! t1 (term s)
+             (! t2 (term s)
+               (term s))))))
+
+; let/flet
+(declare let (! s sort
+             (! t (term s)
+             (! f (! v (term s) formula)
+               formula))))
+(declare flet (! f1 formula
+              (! f2 (! v formula formula)
+                formula)))
+
+; predicates
+(declare = (! s sort
+           (! x (term s)
+           (! y (term s)
+             formula))))
+
+; To avoid duplicating some of the rules (e.g., cong), we will view
+; applications of predicates as terms of sort "Bool".
+; Such terms can be injected as atomic formulas using "p_app".
+
+(declare Bool sort)				; the special sort for predicates
+(declare p_app (! x (term Bool) formula))	; propositional application of term
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Examples
+
+; an example of "(p1 or p2(0)) and t1=t2(1)"
+;(! p1 (term Bool)
+;(! p2 (term (arrow Int Bool))
+;(! t1 (term Int)
+;(! t2 (term (arrow Int Int))
+;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0)))
+;                    (= _ t1 (apply _ _ t2 1))))
+;  ...
+
+; another example of "p3(a,b)"
+;(! a (term Int)
+;(! b (term Int)
+;(! p3 (term (arrow Int (arrow Int Bool)))	; arrow is right assoc.
+;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc.
+;  ...
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; Natural deduction rules : used for CNF
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+
+;; contradiction
+
+(declare contra
+  (! f formula
+  (! r1 (th_holds f)
+  (! r2 (th_holds (not f))
+    (th_holds false)))))
+
+;; not not
+
+(declare not_not_intro
+  (! f formula
+  (! u (th_holds f)
+    (th_holds (not (not f))))))
+    
+(declare not_not_elim
+  (! f formula
+  (! u (th_holds (not (not f)))
+    (th_holds f))))
+
+;; or elimination
+
+(declare or_elim_1
+  (! f1 formula
+  (! f2 formula
+  (! u1 (th_holds (not f1))
+  (! u2 (th_holds (or f1 f2))
+    (th_holds f2))))))
+    
+(declare or_elim_2
+  (! f1 formula
+  (! f2 formula
+  (! u1 (th_holds (not f2))
+  (! u2 (th_holds (or f1 f2))
+    (th_holds f1))))))
+    
+;; and elimination
+
+(declare and_elim_1
+  (! f1 formula
+  (! f2 formula
+  (! u (th_holds (and f1 f2))
+    (th_holds f1)))))
+    
+(declare and_elim_2
+  (! f1 formula
+  (! f2 formula
+  (! u (th_holds (and f1 f2))
+    (th_holds f2)))))
+    
+;; not impl elimination
+
+(declare not_impl_elim_1
+  (! f1 formula
+  (! f2 formula
+  (! u (th_holds (not (impl f1 f2)))
+    (th_holds f1)))))
+    
+(declare not_impl_elim_2
+  (! f1 formula
+  (! f2 formula
+  (! u (th_holds (not (impl f1 f2)))
+    (th_holds (not f2))))))
+    
+;; impl elimination
+
+(declare impl_intro (! f1 formula
+                    (! f2 formula
+                    (! i1 (! u (th_holds f1) 
+                              (th_holds f2))
+                      (th_holds (impl f1 f2))))))
+
+(declare impl_elim
+  (! f1 formula
+  (! f2 formula
+  (! u1 (th_holds f1)
+  (! u2 (th_holds (impl f1 f2))  
+    (th_holds f2))))))
+    
+;; iff elimination
+
+(declare iff_elim_1
+  (! f1 formula
+  (! f2 formula
+  (! u1 (th_holds (iff f1 f2))
+    (th_holds (impl f1 f2))))))
+    
+(declare iff_elim_2
+  (! f1 formula
+  (! f2 formula
+  (! u1 (th_holds (iff f1 f2))
+    (th_holds (impl f2 f1))))))
+
+(declare not_iff_elim_1
+  (! f1 formula
+  (! f2 formula
+  (! u1 (th_holds (not f1))
+  (! u2 (th_holds (not (iff f1 f2)))
+    (th_holds f2))))))
+
+(declare not_iff_elim_2
+  (! f1 formula
+  (! f2 formula
+  (! u1 (th_holds f1)
+  (! u2 (th_holds (not (iff f1 f2)))
+    (th_holds (not f2)))))))
+
+;; ite elimination
+
+(declare ite_elim_1
+  (! a formula
+  (! b formula
+  (! c formula
+  (! u1 (th_holds a)
+  (! u2 (th_holds (ifte a b c))
+    (th_holds b)))))))
+    
+(declare ite_elim_2
+  (! a formula
+  (! b formula
+  (! c formula
+  (! u1 (th_holds (not a))
+  (! u2 (th_holds (ifte a b c))
+    (th_holds c)))))))
+    
+(declare ite_elim_3
+  (! a formula
+  (! b formula
+  (! c formula
+  (! u1 (th_holds (not b))
+  (! u2 (th_holds (ifte a b c))
+    (th_holds c)))))))
+    
+(declare ite_elim_2n
+  (! a formula
+  (! b formula
+  (! c formula
+  (! u1 (th_holds a)
+  (! u2 (th_holds (ifte (not a) b c))
+    (th_holds c)))))))
+
+(declare not_ite_elim_1
+  (! a formula
+  (! b formula
+  (! c formula
+  (! u1 (th_holds a)
+  (! u2 (th_holds (not (ifte a b c)))
+    (th_holds (not b))))))))
+    
+(declare not_ite_elim_2
+  (! a formula
+  (! b formula
+  (! c formula
+  (! u1 (th_holds (not a))
+  (! u2 (th_holds (not (ifte a b c)))
+    (th_holds (not c))))))))
+    
+(declare not_ite_elim_3
+  (! a formula
+  (! b formula
+  (! c formula
+  (! u1 (th_holds b)
+  (! u2 (th_holds (not (ifte a b c)))
+    (th_holds (not c))))))))
+    
+(declare not_ite_elim_2n
+  (! a formula
+  (! b formula
+  (! c formula
+  (! u1 (th_holds a)
+  (! u2 (th_holds (not (ifte (not a) b c)))
+    (th_holds (not c))))))))
+    
+    
+    
+;; How to do CNF for disjunctions of theory literals.
+;;
+;; Given theory literals F1....Fn, and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))).
+;;
+;; We introduce atoms a1...an for literals F1...Fn, mapping them to boolean literals v1...vn.
+;; Do this at the beginning of the proof:
+;;
+;; (decl_atom F1 (\ v1 (\ a1
+;; (decl_atom F2 (\ v2 (\ a2
+;; ....
+;; (decl_atom Fn (\ vn (\ an
+;;
+;; Our input A is clausified by the following proof:
+;;
+;;(satlem _ _
+;;(asf _ _ _ a1 (\ l1
+;;(asf _ _ _ a2 (\ l2
+;;...
+;;(asf _ _ _ an (\ ln
+;;(clausify_false
+;;
+;;   (contra _
+;;      (or_elim_1 _ _ l{n-1}
+;;	...
+;;      (or_elim_1 _ _ l2 
+;; 	(or_elim_1 _ _ l1 A))))) ln)
+;;	
+;;))))))) (\ C
+;;
+;; We now have the free variable C, which should be the clause (v1 V ... V vn).
+;;
+;; We also need to consider the polarity of literals, say we have A of the form (th_holds (or (not F1) (or F2 (not F3)))).
+;; Where necessary, we use "ast" instead of "asf", introduce negations by "not_not_intro" for pattern matching, and flip
+;; the arguments of contra:
+;;
+;;(satlem _ _
+;;(ast _ _ _ a1 (\ l1
+;;(asf _ _ _ a2 (\ l2
+;;(ast _ _ _ a3 (\ l3
+;;(clausify_false
+;;
+;;   (contra _ l3
+;;      (or_elim_1 _ _ l2 
+;; 	(or_elim_1 _ _ (not_not_intro l1) A))))
+;;	
+;;))))))) (\ C
+;;
+;; C should be the clause (~v1 V v2 V ~v3 )
\ No newline at end of file