diff options
-rwxr-xr-x | proofs/signatures/example-quant.plf | 95 | ||||
-rwxr-xr-x | proofs/signatures/th_quant.plf | 86 |
2 files changed, 153 insertions, 28 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)) + +)))))))))))))))))) diff --git a/proofs/signatures/th_quant.plf b/proofs/signatures/th_quant.plf index d18812380..98b53e43d 100755 --- a/proofs/signatures/th_quant.plf +++ b/proofs/signatures/th_quant.plf @@ -3,39 +3,69 @@ (! f formula
formula))))
-(program instantiate ((f formula) (t term) (k term))
- (do (markvar t)
- (let f1 (inst_f f t)
- (do (markvar t) f1))))
+(program eqterm ((n1 term) (n2 term)) bool
+ (do (markvar n1)
+ (let s (ifmarked n2 tt ff)
+ (do (markvar n1) s))))
-(program instantiate_f ((f formula) (k term)) formula
- (match f
- ((and f1 f2) (and (instantiate_f f1 t) (instantiate_f f2 t)))
- ((or f1 f2) (or (instantiate_f f1 t) (instantiate_f f2 t)))
- ((impl f1 f2) (impl (instantiate_f f1 t) (instantiate_f f2 t)))
- ((not f1) (not (instantiate_f f1 t)))
- ((iff f1 f2) (iff (instantiate_f f1 t) (instantiate_f f2 t)))
- ((xor f1 f2) (xor (instantiate_f f1 t) (instantiate_f f2 t)))
- ((ifte f1 f2 f3) (ifte (instantiate_f f1 t) (instantiate_f f2 t) (instantiate_f f3 t)))
- ((= s t1 t2) (= s (inst_t t1 t) (inst_t t2 t)))
- ((forall t1 f1) (forall t1 (instantiate_f f1 t)))
- (default f)))
-
-(program instantiate_t ((t term) (k term)) formula
+(program is_inst_t ((ti term) (t term) (k term)) bool
(match t
- ((apply s1 s2 t1 t2) (apply s1 s2 t1 (instantiate_t t2 t)))
- (default (ifmarked t k t))))
+ ((apply s1 s2 t1 t2)
+ (match ti
+ ((apply si1 si2 ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))
+ (default ff)))
+ (default
+ (match ti
+ ((apply si1 si2 ti1 ti2) ff)
+ (default (eqterm ti (ifmarked t k t)))))))
+
+(program is_inst_f ((fi formula) (f formula) (k term)) bool
+ (match f
+ ((and f1 f2) (match fi
+ ((and fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
+ (default ff)))
+ ((or f1 f2) (match fi
+ ((or fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
+ (default ff)))
+ ((impl f1 f2) (match fi
+ ((impl fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
+ (default ff)))
+ ((not f1) (match fi
+ ((not fi1) (is_inst_f fi1 f1 k))
+ (default ff)))
+ ((iff f1 f2) (match fi
+ ((iff fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
+ (default ff)))
+ ((xor f1 f2) (match fi
+ ((xor fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
+ (default ff)))
+ ((ifte f1 f2 f3) (match fi
+ ((ifte fi1 fi2 fi3) (match (is_inst_f fi1 f1 k)
+ (tt (match (is_inst_f fi2 f2 k) (tt (is_inst_f fi3 f3 k)) (ff ff)))
+ (ff ff)))
+ (default ff)))
+ ((= s t1 t2) (match fi
+ ((= s ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))
+ (default ff)))
+ ((forall s t1 f1) (match fi
+ ((forall s ti1 fi1) (is_inst_f fi1 f1 k))
+ (default ff)))
+ (default ff)))
+(program is_inst ((fi formula) (f formula) (t term) (k term)) bool
+ (do (markvar t)
+ (let f1 (is_inst_f fi f k)
+ (do (markvar t) f1))))
(declare skolem
(! s sort
(! t (term s)
(! f formula
(! p (th_holds (not (forall s t f)))
- (! u (! f1 formula
- (! k (term s)
- (! r (^ (instantiate f t k) f1)
- (! p1 (th_holds (not f1))
+ (! u (! k (term s)
+ (! fi formula
+ (! p1 (th_holds (not fi))
+ (! r (^ (is_inst fi f t k) tt)
(holds cln)))))
(holds cln)))))))
@@ -43,10 +73,10 @@ (! s sort
(! t (term s)
(! f formula
- (! f1 formula
- (! p (th_holds (forall s t f))
(! k (term s)
- (! r (^ (instantiate f t k) f1)
- (! u (! p1 (th_holds f1)
+ (! fi formula
+ (! p (th_holds (forall s t f))
+ (! r (^ (is_inst fi f t k) tt)
+ (! u (! p1 (th_holds fi)
(holds cln))
(holds cln))))))))))
\ No newline at end of file |