diff options
Diffstat (limited to 'proofs/signatures/smt.plf')
-rwxr-xr-x | proofs/signatures/smt.plf | 313 |
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 |