diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/signatures/Makefile.am | 34 | ||||
| -rwxr-xr-x | proofs/signatures/example.plf | 232 | ||||
| -rwxr-xr-x | proofs/signatures/sat.plf | 254 | ||||
| -rwxr-xr-x | proofs/signatures/smt.plf | 48 | ||||
| -rwxr-xr-x | proofs/signatures/th_base.plf | 214 |
5 files changed, 408 insertions, 374 deletions
diff --git a/proofs/signatures/Makefile.am b/proofs/signatures/Makefile.am new file mode 100644 index 000000000..610990ba2 --- /dev/null +++ b/proofs/signatures/Makefile.am @@ -0,0 +1,34 @@ +# These CORE_PLFs are combined to give a "master signature" against +# which proofs are checked internally when using --check-proofs. To +# add support for more theories, just list them here in the same order +# you would to the LFSC proof-checker binary. +# +CORE_PLFS = sat.plf smt.plf th_base.plf + +noinst_LTLIBRARIES = libsignatures.la + +dist_pkgdata_DATA = \ + $(CORE_PLFS) + +libsignatures_la_SOURCES = \ + signatures.cpp + +BUILT_SOURCES = \ + signatures.cpp + +signatures.cpp: $(CORE_PLFS) + $(AM_V_GEN)( \ + echo "namespace CVC4 {"; \ + echo "namespace proof {"; \ + echo; \ + echo "extern const char *const plf_signatures;"; \ + echo "const char *const plf_signatures = \"\\"; \ + cat $+ | sed 's,\\,\\\\,g;s,",\\",g;s,$$,\\n\\,g'; \ + echo "\";"; \ + echo; \ + echo "} /* CVC4::proof namespace */"; \ + echo "} /* CVC4 namespace */"; \ + ) > $@ + +EXTRA_DIST = \ + example.plf diff --git a/proofs/signatures/example.plf b/proofs/signatures/example.plf index 5df1f31c3..ab690eb51 100755 --- a/proofs/signatures/example.plf +++ b/proofs/signatures/example.plf @@ -1,116 +1,116 @@ -; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf
-
-; --------------------------------------------------------------------------------
-; input :
-; ( a = b )
-; ( b = f(c) )
-; ( a != f(c) V a != b )
-
-; theory lemma (by transitivity) :
-; ( a != b V b != f(c) V a = f(c) )
-
-
-; With the theory lemma, the input is unsatisfiable.
-; --------------------------------------------------------------------------------
-
-
-
-(check
-(% s sort
-(% a (term s)
-(% b (term s)
-(% c (term s)
-(% f (term (arrow s s))
-
-; -------------------- declaration of input formula -----------------------------------
-
-(% A1 (th_holds (= s a b))
-(% A2 (th_holds (= s b (apply _ _ f c)))
-(% A3 (th_holds (or (not (= s a (apply _ _ f c))) (not (= s a b))))
-
-
-; ------------------- specify that the following is a proof of the empty clause -----------------
-
-(: (holds cln)
-
-; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------
-
-(decl_atom (= s a b) (\ v1 (\ a1
-(decl_atom (= s b (apply _ _ f c)) (\ v2 (\ a2
-(decl_atom (= s a (apply _ _ f c)) (\ v3 (\ a3
-
-
-; --------------------------- proof of theory lemma ---------------------------------------------
-
-(satlem _ _
-(ast _ _ _ a1 (\ l1
-(ast _ _ _ a2 (\ l2
-(asf _ _ _ a3 (\ l3
-(clausify_false
-
-; this should be a proof of l1 ^ l2 ^ ~l3 => false
-; this is done by theory proof rules (currently just use "trust")
-
- trust
-
-))))))) (\ CT
-; CT is the clause ( ~v1 V ~v2 V v3 )
-
-; -------------------- clausification of input formulas -----------------------------------------
-
-(satlem _ _
-(asf _ _ _ a1 (\ l1
-(clausify_false
-
-; input formula A1 is ( ~l1 )
-; the following should be a proof of l1 ^ ( ~l1 ) => false
-; this is done by natural deduction rules
-
- (contra _ A1 l1)
-
-))) (\ C1
-; C1 is the clause ( v1 )
-
-
-(satlem _ _
-(asf _ _ _ a2 (\ l2
-(clausify_false
-
-; input formula A2 is ( ~l2 )
-; the following should be a proof of l2 ^ ( ~l2 ) => false
-; this is done by natural deduction rules
-
- (contra _ A2 l2)
-
-))) (\ C2
-; C2 is the clause ( v2 )
-
-
-(satlem _ _
-(ast _ _ _ a3 (\ l3
-(ast _ _ _ a1 (\ l1
-(clausify_false
-
-; input formula A3 is ( ~a3 V ~a1 )
-; the following should be a proof of a3 ^ a1 ^ ( ~a3 V ~a1 ) => false
-; this is done by natural deduction rules
-
- (contra _ l1 (or_elim_1 _ _ (not_not_intro _ l3) A3))
-
-))))) (\ C3
-; C3 is the clause ( ~v3 V ~v1 )
-
-
-
-; -------------------- resolution proof ------------------------------------------------------------
-
-(satlem_simplify _ _ _
-
-(R _ _ C1
-(R _ _ C2
-(R _ _ CT C3 v3) v2) v1)
-
-(\ x x))
-
-))))))))))))))))))))))))))
-)
\ No newline at end of file +; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf + +; -------------------------------------------------------------------------------- +; input : +; ( a = b ) +; ( b = f(c) ) +; ( a != f(c) V a != b ) + +; theory lemma (by transitivity) : +; ( a != b V b != f(c) V a = f(c) ) + + +; With the theory lemma, the input is unsatisfiable. +; -------------------------------------------------------------------------------- + + + +(check +(% s sort +(% a (term s) +(% b (term s) +(% c (term s) +(% f (term (arrow s s)) + +; -------------------- declaration of input formula ----------------------------------- + +(% A1 (th_holds (= s a b)) +(% A2 (th_holds (= s b (apply _ _ f c))) +(% A3 (th_holds (or (not (= s a (apply _ _ f c))) (not (= s a b)))) + + +; ------------------- specify that the following is a proof of the empty clause ----------------- + +(: (holds cln) + +; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------ + +(decl_atom (= s a b) (\ v1 (\ a1 +(decl_atom (= s b (apply _ _ f c)) (\ v2 (\ a2 +(decl_atom (= s a (apply _ _ f c)) (\ v3 (\ a3 + + +; --------------------------- proof of theory lemma --------------------------------------------- + +(satlem _ _ +(ast _ _ _ a1 (\ l1 +(ast _ _ _ a2 (\ l2 +(asf _ _ _ a3 (\ l3 +(clausify_false + +; this should be a proof of l1 ^ l2 ^ ~l3 => false +; this is done by theory proof rules (currently just use "trust") + + trust + +))))))) (\ CT +; CT is the clause ( ~v1 V ~v2 V v3 ) + +; -------------------- clausification of input formulas ----------------------------------------- + +(satlem _ _ +(asf _ _ _ a1 (\ l1 +(clausify_false + +; input formula A1 is ( ~l1 ) +; the following should be a proof of l1 ^ ( ~l1 ) => false +; this is done by natural deduction rules + + (contra _ A1 l1) + +))) (\ C1 +; C1 is the clause ( v1 ) + + +(satlem _ _ +(asf _ _ _ a2 (\ l2 +(clausify_false + +; input formula A2 is ( ~l2 ) +; the following should be a proof of l2 ^ ( ~l2 ) => false +; this is done by natural deduction rules + + (contra _ A2 l2) + +))) (\ C2 +; C2 is the clause ( v2 ) + + +(satlem _ _ +(ast _ _ _ a3 (\ l3 +(ast _ _ _ a1 (\ l1 +(clausify_false + +; input formula A3 is ( ~a3 V ~a1 ) +; the following should be a proof of a3 ^ a1 ^ ( ~a3 V ~a1 ) => false +; this is done by natural deduction rules + + (contra _ l1 (or_elim_1 _ _ (not_not_intro _ l3) A3)) + +))))) (\ C3 +; C3 is the clause ( ~v3 V ~v1 ) + + + +; -------------------- resolution proof ------------------------------------------------------------ + +(satlem_simplify _ _ _ + +(R _ _ C1 +(R _ _ C2 +(R _ _ CT C3 v3) v2) v1) + +(\ x x)) + +)))))))))))))))))))))))))) +) diff --git a/proofs/signatures/sat.plf b/proofs/signatures/sat.plf index 09255f612..5e2f1cc44 100755 --- a/proofs/signatures/sat.plf +++ b/proofs/signatures/sat.plf @@ -1,127 +1,127 @@ -(declare bool type)
-(declare tt bool)
-(declare ff bool)
-
-(declare var type)
-
-(declare lit type)
-(declare pos (! x var lit))
-(declare neg (! x var lit))
-
-(declare clause type)
-(declare cln clause)
-(declare clc (! x lit (! c clause clause)))
-
-; constructs for general clauses for R, Q, satlem
-
-(declare concat (! c1 clause (! c2 clause clause)))
-(declare clr (! l lit (! c clause clause)))
-
-; code to check resolutions
-
-(program append ((c1 clause) (c2 clause)) clause
- (match c1 (cln c2) ((clc l c1') (clc l (append c1' c2)))))
-
-; we use marks as follows:
-; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable.
-; -- mark 2 to record if we are supposed to remove a negative occurrence of the variable.
-; -- mark 3 if we did indeed remove the variable positively
-; -- mark 4 if we did indeed remove the variable negatively
-(program simplify_clause ((c clause)) clause
- (match c
- (cln cln)
- ((clc l c1)
- (match l
- ; Set mark 1 on v if it is not set, to indicate we should remove it.
- ; After processing the rest of the clause, set mark 3 if we were already
- ; supposed to remove v (so if mark 1 was set when we began). Clear mark3
- ; if we were not supposed to be removing v when we began this call.
- ((pos v)
- (let m (ifmarked v tt (do (markvar v) ff))
- (let c' (simplify_clause c1)
- (match m
- (tt (do (ifmarked3 v v (markvar3 v)) c'))
- (ff (do (ifmarked3 v (markvar3 v) v) (markvar v) (clc l c')))))))
- ; the same as the code for tt, but using different marks.
- ((neg v)
- (let m (ifmarked2 v tt (do (markvar2 v) ff))
- (let c' (simplify_clause c1)
- (match m
- (tt (do (ifmarked4 v v (markvar4 v)) c'))
- (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c')))))))))
- ((concat c1 c2) (append (simplify_clause c1) (simplify_clause c2)))
- ((clr l c1)
- (match l
- ; set mark 1 to indicate we should remove v, and fail if
- ; mark 3 is not set after processing the rest of the clause
- ; (we will set mark 3 if we remove a positive occurrence of v).
- ((pos v)
- (let m (ifmarked v tt (do (markvar v) ff))
- (let m3 (ifmarked3 v (do (markvar3 v) tt) ff)
- (let c' (simplify_clause c1)
- (ifmarked3 v (do (match m3 (tt v) (ff (markvar3 v)))
- (match m (tt v) (ff (markvar v))) c')
- (fail clause))))))
- ; same as the tt case, but with different marks.
- ((neg v)
- (let m2 (ifmarked2 v tt (do (markvar2 v) ff))
- (let m4 (ifmarked4 v (do (markvar4 v) tt) ff)
- (let c' (simplify_clause c1)
- (ifmarked4 v (do (match m4 (tt v) (ff (markvar4 v)))
- (match m2 (tt v) (ff (markvar2 v))) c')
- (fail clause))))))
- ))))
-
-
-; resolution proofs
-
-(declare holds (! c clause type))
-
-(declare R (! c1 clause (! c2 clause
- (! u1 (holds c1)
- (! u2 (holds c2)
- (! n var
- (holds (concat (clr (pos n) c1)
- (clr (neg n) c2)))))))))
-
-(declare Q (! c1 clause (! c2 clause
- (! u1 (holds c1)
- (! u2 (holds c2)
- (! n var
- (holds (concat (clr (neg n) c1)
- (clr (pos n) c2)))))))))
-
-(declare satlem_simplify
- (! c1 clause
- (! c2 clause
- (! c3 clause
- (! u1 (holds c1)
- (! r (^ (simplify_clause c1) c2)
- (! u2 (! x (holds c2) (holds c3))
- (holds c3))))))))
-
-(declare satlem
- (! c clause
- (! c2 clause
- (! u (holds c)
- (! u2 (! v (holds c) (holds c2))
- (holds c2))))))
-
-; A little example to demonstrate simplify_clause.
-; It can handle nested clr's of both polarities,
-; and correctly cleans up marks when it leaves a
-; clr or clc scope. Uncomment and run with
-; --show-runs to see it in action.
-;
-; (check
-; (% v1 var
-; (% u1 (holds (concat (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln))))))
-; (clc (pos v1) (clc (pos v1) cln))))
-; (satlem _ _ _ u1 (\ x x))))))
-
-
-;(check
-; (% v1 var
-; (% u1 (holds (clr (neg v1) (concat (clc (neg v1) cln)
-; (clr (neg v1) (clc (neg v1) cln)))))
-; (satlem _ _ _ u1 (\ x x))))))
\ No newline at end of file +(declare bool type) +(declare tt bool) +(declare ff bool) + +(declare var type) + +(declare lit type) +(declare pos (! x var lit)) +(declare neg (! x var lit)) + +(declare clause type) +(declare cln clause) +(declare clc (! x lit (! c clause clause))) + +; constructs for general clauses for R, Q, satlem + +(declare concat (! c1 clause (! c2 clause clause))) +(declare clr (! l lit (! c clause clause))) + +; code to check resolutions + +(program append ((c1 clause) (c2 clause)) clause + (match c1 (cln c2) ((clc l c1') (clc l (append c1' c2))))) + +; we use marks as follows: +; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable. +; -- mark 2 to record if we are supposed to remove a negative occurrence of the variable. +; -- mark 3 if we did indeed remove the variable positively +; -- mark 4 if we did indeed remove the variable negatively +(program simplify_clause ((c clause)) clause + (match c + (cln cln) + ((clc l c1) + (match l + ; Set mark 1 on v if it is not set, to indicate we should remove it. + ; After processing the rest of the clause, set mark 3 if we were already + ; supposed to remove v (so if mark 1 was set when we began). Clear mark3 + ; if we were not supposed to be removing v when we began this call. + ((pos v) + (let m (ifmarked v tt (do (markvar v) ff)) + (let c' (simplify_clause c1) + (match m + (tt (do (ifmarked3 v v (markvar3 v)) c')) + (ff (do (ifmarked3 v (markvar3 v) v) (markvar v) (clc l c'))))))) + ; the same as the code for tt, but using different marks. + ((neg v) + (let m (ifmarked2 v tt (do (markvar2 v) ff)) + (let c' (simplify_clause c1) + (match m + (tt (do (ifmarked4 v v (markvar4 v)) c')) + (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c'))))))))) + ((concat c1 c2) (append (simplify_clause c1) (simplify_clause c2))) + ((clr l c1) + (match l + ; set mark 1 to indicate we should remove v, and fail if + ; mark 3 is not set after processing the rest of the clause + ; (we will set mark 3 if we remove a positive occurrence of v). + ((pos v) + (let m (ifmarked v tt (do (markvar v) ff)) + (let m3 (ifmarked3 v (do (markvar3 v) tt) ff) + (let c' (simplify_clause c1) + (ifmarked3 v (do (match m3 (tt v) (ff (markvar3 v))) + (match m (tt v) (ff (markvar v))) c') + (fail clause)))))) + ; same as the tt case, but with different marks. + ((neg v) + (let m2 (ifmarked2 v tt (do (markvar2 v) ff)) + (let m4 (ifmarked4 v (do (markvar4 v) tt) ff) + (let c' (simplify_clause c1) + (ifmarked4 v (do (match m4 (tt v) (ff (markvar4 v))) + (match m2 (tt v) (ff (markvar2 v))) c') + (fail clause)))))) + )))) + + +; resolution proofs + +(declare holds (! c clause type)) + +(declare R (! c1 clause (! c2 clause + (! u1 (holds c1) + (! u2 (holds c2) + (! n var + (holds (concat (clr (pos n) c1) + (clr (neg n) c2))))))))) + +(declare Q (! c1 clause (! c2 clause + (! u1 (holds c1) + (! u2 (holds c2) + (! n var + (holds (concat (clr (neg n) c1) + (clr (pos n) c2))))))))) + +(declare satlem_simplify + (! c1 clause + (! c2 clause + (! c3 clause + (! u1 (holds c1) + (! r (^ (simplify_clause c1) c2) + (! u2 (! x (holds c2) (holds c3)) + (holds c3)))))))) + +(declare satlem + (! c clause + (! c2 clause + (! u (holds c) + (! u2 (! v (holds c) (holds c2)) + (holds c2)))))) + +; A little example to demonstrate simplify_clause. +; It can handle nested clr's of both polarities, +; and correctly cleans up marks when it leaves a +; clr or clc scope. Uncomment and run with +; --show-runs to see it in action. +; +; (check +; (% v1 var +; (% u1 (holds (concat (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln)))))) +; (clc (pos v1) (clc (pos v1) cln)))) +; (satlem _ _ _ u1 (\ x x)))))) + + +;(check +; (% v1 var +; (% u1 (holds (clr (neg v1) (concat (clc (neg v1) cln) +; (clr (neg v1) (clc (neg v1) cln))))) +; (satlem _ _ _ u1 (\ x x)))))) diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf index 75bfc442f..67ce3988a 100755 --- a/proofs/signatures/smt.plf +++ b/proofs/signatures/smt.plf @@ -31,7 +31,7 @@ (! t1 (term (arrow s1 s2)) (! t2 (term s1) (term s2)))))) - + (declare ite (! s sort (! f formula (! t1 (term s) @@ -102,7 +102,7 @@ (! f formula (! u (th_holds f) (th_holds (not (not f)))))) - + (declare not_not_elim (! f formula (! u (th_holds (not (not f))) @@ -116,14 +116,14 @@ (! 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 @@ -131,13 +131,13 @@ (! 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 @@ -145,18 +145,18 @@ (! 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) + (! i1 (! u (th_holds f1) (th_holds f2)) (th_holds (impl f1 f2)))))) @@ -164,9 +164,9 @@ (! f1 formula (! f2 formula (! u1 (th_holds f1) - (! u2 (th_holds (impl f1 f2)) + (! u2 (th_holds (impl f1 f2)) (th_holds f2)))))) - + ;; iff elimination (declare iff_elim_1 @@ -174,7 +174,7 @@ (! f2 formula (! u1 (th_holds (iff f1 f2)) (th_holds (impl f1 f2)))))) - + (declare iff_elim_2 (! f1 formula (! f2 formula @@ -204,7 +204,7 @@ (! u1 (th_holds a) (! u2 (th_holds (ifte a b c)) (th_holds b))))))) - + (declare ite_elim_2 (! a formula (! b formula @@ -212,7 +212,7 @@ (! u1 (th_holds (not a)) (! u2 (th_holds (ifte a b c)) (th_holds c))))))) - + (declare ite_elim_3 (! a formula (! b formula @@ -220,7 +220,7 @@ (! u1 (th_holds (not b)) (! u2 (th_holds (ifte a b c)) (th_holds c))))))) - + (declare ite_elim_2n (! a formula (! b formula @@ -236,7 +236,7 @@ (! 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 @@ -244,7 +244,7 @@ (! 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 @@ -252,7 +252,7 @@ (! 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 @@ -260,9 +260,9 @@ (! 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))))). @@ -287,7 +287,7 @@ ;; (contra _ ;; (or_elim_1 _ _ l{n-1} ;; ... -;; (or_elim_1 _ _ l2 +;; (or_elim_1 _ _ l2 ;; (or_elim_1 _ _ l1 A))))) ln) ;; ;;))))))) (\ C @@ -305,9 +305,9 @@ ;;(clausify_false ;; ;; (contra _ l3 -;; (or_elim_1 _ _ l2 +;; (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 +;; C should be the clause (~v1 V v2 V ~v3 ) diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf index e66990de4..7b0b086dc 100755 --- a/proofs/signatures/th_base.plf +++ b/proofs/signatures/th_base.plf @@ -1,107 +1,107 @@ -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Atomization / Clausification
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-; binding between an LF var and an (atomic) formula
-(declare atom (! v var (! p formula type)))
-
-(declare decl_atom
- (! f formula
- (! u (! v var
- (! a (atom v f)
- (holds cln)))
- (holds cln))))
-
-; direct clausify
-(declare clausify_form
- (! f formula
- (! v var
- (! a (atom v f)
- (! u (th_holds f)
- (holds (clc (pos v) cln)))))))
-
-(declare clausify_form_not
- (! f formula
- (! v var
- (! a (atom v f)
- (! u (th_holds (not f))
- (holds (clc (neg v) cln)))))))
-
-(declare clausify_false
- (! u (th_holds false)
- (holds cln)))
-
-
-(declare th_let_pf
- (! f formula
- (! u (th_holds f)
- (! u2 (! v (th_holds f) (holds cln))
- (holds cln)))))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Theory reasoning
-; - make a series of assumptions and then derive a contradiction (or false)
-; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"
-; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(declare ast
- (! v var
- (! f formula
- (! C clause
- (! r (atom v f) ;this is specified
- (! u (! o (th_holds f)
- (holds C))
- (holds (clc (neg v) C))))))))
-
-(declare asf
- (! v var
- (! f formula
- (! C clause
- (! r (atom v f)
- (! u (! o (th_holds (not f))
- (holds C))
- (holds (clc (pos v) C))))))))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Theory of Equality and Congruence Closure
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-; temporary :
-(declare trust (th_holds false))
-
-(declare refl
- (! s sort
- (! t (term s)
- (th_holds (= s t t)))))
-
-(declare symm (! s sort
- (! x (term s)
- (! y (term s)
- (! u (th_holds (= _ x y))
- (th_holds (= _ y x)))))))
-
-(declare trans (! s sort
- (! x (term s)
- (! y (term s)
- (! z (term s)
- (! u (th_holds (= _ x y))
- (! u (th_holds (= _ y z))
- (th_holds (= _ x z)))))))))
-
-(declare cong (! s1 sort
- (! s2 sort
- (! a1 (term (arrow s1 s2))
- (! b1 (term (arrow s1 s2))
- (! a2 (term s1)
- (! b2 (term s1)
- (! u1 (th_holds (= _ a1 b1))
- (! u2 (th_holds (= _ a2 b2))
- (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2))))))))))))
-
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; +; Atomization / Clausification +; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; binding between an LF var and an (atomic) formula +(declare atom (! v var (! p formula type))) + +(declare decl_atom + (! f formula + (! u (! v var + (! a (atom v f) + (holds cln))) + (holds cln)))) + +; direct clausify +(declare clausify_form + (! f formula + (! v var + (! a (atom v f) + (! u (th_holds f) + (holds (clc (pos v) cln))))))) + +(declare clausify_form_not + (! f formula + (! v var + (! a (atom v f) + (! u (th_holds (not f)) + (holds (clc (neg v) cln))))))) + +(declare clausify_false + (! u (th_holds false) + (holds cln))) + + +(declare th_let_pf + (! f formula + (! u (th_holds f) + (! u2 (! v (th_holds f) (holds cln)) + (holds cln))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; +; Theory reasoning +; - make a series of assumptions and then derive a contradiction (or false) +; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false" +; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn" +; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(declare ast + (! v var + (! f formula + (! C clause + (! r (atom v f) ;this is specified + (! u (! o (th_holds f) + (holds C)) + (holds (clc (neg v) C)))))))) + +(declare asf + (! v var + (! f formula + (! C clause + (! r (atom v f) + (! u (! o (th_holds (not f)) + (holds C)) + (holds (clc (pos v) C)))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; +; Theory of Equality and Congruence Closure +; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; temporary : +(declare trust (th_holds false)) + +(declare refl + (! s sort + (! t (term s) + (th_holds (= s t t))))) + +(declare symm (! s sort + (! x (term s) + (! y (term s) + (! u (th_holds (= _ x y)) + (th_holds (= _ y x))))))) + +(declare trans (! s sort + (! x (term s) + (! y (term s) + (! z (term s) + (! u (th_holds (= _ x y)) + (! u (th_holds (= _ y z)) + (th_holds (= _ x z))))))))) + +(declare cong (! s1 sort + (! s2 sort + (! a1 (term (arrow s1 s2)) + (! b1 (term (arrow s1 s2)) + (! a2 (term s1) + (! b2 (term s1) + (! u1 (th_holds (= _ a1 b1)) + (! u2 (th_holds (= _ a2 b2)) + (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2)))))))))))) + |