diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-10-03 09:52:24 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-03 10:55:14 -0500 |
| commit | 38503bde0d58e80bd6c39152fb7d2f226d8ac3c9 (patch) | |
| tree | 75e0bc7ebf8d7da29d04ca9f36ebb130bf5bec45 /proofs/signatures/th_base.plf | |
| parent | b663c658c80cee918afe37222e62dd1e5db33f5c (diff) | |
Adding example proof signatures for LFSC.
Diffstat (limited to 'proofs/signatures/th_base.plf')
| -rwxr-xr-x | proofs/signatures/th_base.plf | 107 |
1 files changed, 107 insertions, 0 deletions
diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf new file mode 100755 index 000000000..e66990de4 --- /dev/null +++ b/proofs/signatures/th_base.plf @@ -0,0 +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))))))))))))
+
|