diff options
Diffstat (limited to 'proofs/signatures')
-rwxr-xr-x | proofs/signatures/example-arrays.plf | 139 | ||||
-rwxr-xr-x | proofs/signatures/th_arrays.plf | 29 | ||||
-rwxr-xr-x | proofs/signatures/th_quant.plf | 52 |
3 files changed, 205 insertions, 15 deletions
diff --git a/proofs/signatures/example-arrays.plf b/proofs/signatures/example-arrays.plf new file mode 100755 index 000000000..600fc11c9 --- /dev/null +++ b/proofs/signatures/example-arrays.plf @@ -0,0 +1,139 @@ +; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf + +; -------------------------------------------------------------------------------- +; literals : +; L1 : a = write( a, i, read( a, i ) +; L2 : read( a, k ) = read( write( a, i, read( a, i ) ), k ) +; L3 : i = k + +; input : +; ~L1 + +; (extenstionality) lemma : +; L1 or ~L2 + +; theory conflicts : +; L2 or ~L3 +; L2 or L3 + + +; With the theory lemma, the input is unsatisfiable. +; -------------------------------------------------------------------------------- + + +; (0) -------------------- term declarations ----------------------------------- + +(check +(% I sort +(% E sort +(% a (term (array I E)) +(% i (term I) + + +; (1) -------------------- input formula ----------------------------------- + +(% A1 (th_holds (not (= (array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))))) + + + + +; (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 ...) + + +; extensionality lemma : notice this also introduces skolem k +(ext _ _ a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)) (\ k (\ A2 + + + + +; (4) -------------------- map theory literals to boolean variables +; --- maps all theory literals involved in proof to boolean literals + +(decl_atom (= (array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) (\ v1 (\ a1 +(decl_atom (= E (apply _ _ (apply _ _ (read I E) a) k) (apply _ _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) k)) (\ v2 (\ a2 +(decl_atom (= I i k) (\ v3 (\ a3 + + + +; (5) -------------------- theory conflicts --------------------------------------------- +; --- these should introduce (holds ...) + +(satlem _ _ +(asf _ _ _ a3 (\ l3 +(asf _ _ _ a2 (\ l2 +(clausify_false + + ; use read over write rule "row" + (contra _ (symm _ _ _ (row _ _ _ _ a (apply _ _ (apply _ _ (read I E) a) i) l3)) l2) + +))))) (\ CT1 +; CT1 is the clause ( v2 V v3 ) + +(satlem _ _ +(ast _ _ _ a3 (\ l3 +(asf _ _ _ a2 (\ l2 +(clausify_false + + ; use read over write rule "row1" + (contra _ (symm _ _ _ + (trans _ _ _ _ + (symm _ _ _ (cong _ _ _ _ _ _ + (refl _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)))) + l3)) + (trans _ _ _ _ + (row1 _ _ a i (apply _ _ (apply _ _ (read I E) a) i)) + (cong _ _ _ _ _ _ (refl _ (apply _ _ (read I E) a)) l3) + ))) + l2) + +))))) (\ CT2 +; CT2 is the clause ( v2 V ~v3 ) + + +; (6) -------------------- clausification ----------------------------------------- +; --- these should introduce (holds ...) + +(satlem _ _ +(ast _ _ _ a1 (\ l1 +(clausify_false + +; input formula A1 is ( ~a1 ) +; the following is a proof of a1 ^ ( ~a1 ) => false + + (contra _ l1 A1) + +))) (\ C1 +; C1 is the clause ( ~v1 ) + + +(satlem _ _ +(asf _ _ _ a1 (\ l1 +(ast _ _ _ a2 (\ l2 +(clausify_false + +; lemma A2 is ( a1 V ~a2 ) +; the following is a proof of ~a1 ^ a2 ^ ( a1 V ~a2 ) => false + + (contra _ l2 (or_elim_1 _ _ l1 A2)) + +))))) (\ C2 +; C2 is the clause ( v1 V ~v2 ) + + +; (7) -------------------- resolution proof ------------------------------------------------------------ + +(satlem_simplify _ _ _ + +(R _ _ (R _ _ CT1 CT2 v3) (R _ _ C2 C1 v1) v2) + +(\ x x)) + +))))))))))))))))))))))))))) diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf index 6e0e6438d..edb6dc96e 100755 --- a/proofs/signatures/th_arrays.plf +++ b/proofs/signatures/th_arrays.plf @@ -12,15 +12,14 @@ ; functions
(declare write (! s1 sort
(! s2 sort
- (! t1 (term (array s1 s2))
- (! t2 (term s1)
- (! t3 (term s2)
- (term (array s1 s2))))))))
+ (term (arrow (array s1 s2)
+ (arrow s1
+ (arrow s2 (array s1 s2))))))))
+
(declare read (! s1 sort
(! s2 sort
- (! t1 (term (array s1 s2))
- (! t2 (term s1)
- (term s2))))))
+ (term (arrow (array s1 s2)
+ (arrow s1 s2))))))
; inference rules
(declare row1 (! s1 sort
@@ -28,26 +27,26 @@ (! t1 (term (array s1 s2))
(! t2 (term s1)
(! t3 (term s2)
- (th_holds (= _ (read (write t1 t2 t3) t2) t3))))))))
+ (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t3)) t2)
+ t3))))))))
(declare row (! s1 sort
(! s2 sort
- (! t1 (term (array s1 s2))
(! t2 (term s1)
(! t3 (term s1)
+ (! t1 (term (array s1 s2))
(! t4 (term s2)
(! u (th_holds (not (= _ t2 t3)))
- (th_holds (= _ (read (write t1 t2 t4) t3) (read t1 t3))))))))))
+ (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3)
+ (apply _ _ (apply _ _ (read s1 s2) t1) t3)))))))))))
(declare ext (! s1 sort
(! s2 sort
- (! f formula
(! t1 (term (array s1 s2))
(! t2 (term (array s1 s2))
- (! u (th_holds (not (= _ t1 t2)))
(! u1 (! k (term s1)
- (! u2 (th_holds (not (= _ (read t1 k) (read t2 k))))
- (th_holds f)))
- (th_holds f)))))))))
+ (! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k)))))
+ (holds cln)))
+ (holds cln)))))))
\ No newline at end of file diff --git a/proofs/signatures/th_quant.plf b/proofs/signatures/th_quant.plf new file mode 100755 index 000000000..d18812380 --- /dev/null +++ b/proofs/signatures/th_quant.plf @@ -0,0 +1,52 @@ +(declare forall (! s sort
+ (! t (term s)
+ (! 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 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
+ (match t
+ ((apply s1 s2 t1 t2) (apply s1 s2 t1 (instantiate_t t2 t)))
+ (default (ifmarked t k t))))
+
+
+(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))
+ (holds cln)))))
+ (holds cln)))))))
+
+(declare inst
+ (! 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)
+ (holds cln))
+ (holds cln))))))))))
\ No newline at end of file |