diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-13 09:58:07 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-13 09:58:07 -0500 |
commit | 2b2c656543cc4ee7051ff00211a56f45331a763c (patch) | |
tree | 4e54f86ac7446d32b58282fca362851c716cc151 /proofs/signatures/example-quant.plf | |
parent | 8b41e8d8128752eba75f32f751ec9c095a6b1d87 (diff) |
Add working example of LFSC proof with quantifiers. Update quantifiers signature to avoid dependent types in side condition.
Diffstat (limited to 'proofs/signatures/example-quant.plf')
-rwxr-xr-x | proofs/signatures/example-quant.plf | 95 |
1 files changed, 95 insertions, 0 deletions
diff --git a/proofs/signatures/example-quant.plf b/proofs/signatures/example-quant.plf new file mode 100755 index 000000000..086633be9 --- /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)) + +)))))))))))))))))) |