diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-08-05 18:29:34 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-23 13:21:47 -0500 |
commit | ff7d33c2f75668fde0f149943e3cf1bedad1102f (patch) | |
tree | b2533c2a7bf09602d567379ea1dc3bacc9f059c3 /proofs/signatures/example.plf | |
parent | b2bb2138543e75f64c3a794df940a221e4b5a97b (diff) |
Proof-checking code; fixups of segfaults and missing functionality in proof generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
Diffstat (limited to 'proofs/signatures/example.plf')
-rwxr-xr-x | proofs/signatures/example.plf | 232 |
1 files changed, 116 insertions, 116 deletions
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)) + +)))))))))))))))))))))))))) +) |