|
Jerry James |
17aa174 |
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
Jerry James |
17aa174 |
;
|
|
Jerry James |
17aa174 |
; Atomization
|
|
Jerry James |
17aa174 |
;
|
|
Jerry James |
17aa174 |
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
; binding between an LF var and an (atomic) formula
|
|
Jerry James |
17aa174 |
(declare atom (! v var (! p formula type)))
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
(declare decl_atom
|
|
Jerry James |
17aa174 |
(! f formula
|
|
Jerry James |
17aa174 |
(! u (! v var
|
|
Jerry James |
17aa174 |
(! a (atom v f)
|
|
Jerry James |
17aa174 |
bottom))
|
|
Jerry James |
17aa174 |
bottom)))
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
; direct clausify
|
|
Jerry James |
17aa174 |
(declare clausify_form
|
|
Jerry James |
17aa174 |
(! f formula
|
|
Jerry James |
17aa174 |
(! v var
|
|
Jerry James |
17aa174 |
(! a (atom v f)
|
|
Jerry James |
17aa174 |
(! u (th_holds f)
|
|
Jerry James |
17aa174 |
(holds (clc (pos v) cln)))))))
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
(declare clausify_form_not
|
|
Jerry James |
17aa174 |
(! f formula
|
|
Jerry James |
17aa174 |
(! v var
|
|
Jerry James |
17aa174 |
(! a (atom v f)
|
|
Jerry James |
17aa174 |
(! u (th_holds (not f))
|
|
Jerry James |
17aa174 |
(holds (clc (neg v) cln)))))))
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
(declare clausify_false
|
|
Jerry James |
17aa174 |
(! u (th_holds false)
|
|
Jerry James |
17aa174 |
bottom))
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
(declare let_pf
|
|
Jerry James |
17aa174 |
(! c clause
|
|
Jerry James |
17aa174 |
(! c' clause
|
|
Jerry James |
17aa174 |
(! u (holds c)
|
|
Jerry James |
17aa174 |
(! u2 (! v (holds c) bottom)
|
|
Jerry James |
17aa174 |
bottom)))))
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
(declare th_let_pf
|
|
Jerry James |
17aa174 |
(! f formula
|
|
Jerry James |
17aa174 |
(! u (th_holds f)
|
|
Jerry James |
17aa174 |
(! u2 (! v (th_holds f) bottom)
|
|
Jerry James |
17aa174 |
bottom))))
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
Jerry James |
17aa174 |
;
|
|
Jerry James |
17aa174 |
; Theory reasoning
|
|
Jerry James |
17aa174 |
; - make a series of assumptions and then derive a contradiction (or false)
|
|
Jerry James |
17aa174 |
; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"
|
|
Jerry James |
17aa174 |
; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"
|
|
Jerry James |
17aa174 |
;
|
|
Jerry James |
17aa174 |
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
(declare ast
|
|
Jerry James |
17aa174 |
(! v var
|
|
Jerry James |
17aa174 |
(! f formula
|
|
Jerry James |
17aa174 |
(! C clause
|
|
Jerry James |
17aa174 |
(! r (atom v f) ;this is specified
|
|
Jerry James |
17aa174 |
(! u (! o (th_holds f)
|
|
Jerry James |
17aa174 |
(holds C))
|
|
Jerry James |
17aa174 |
(holds (clc (neg v) C))))))))
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
(declare asf
|
|
Jerry James |
17aa174 |
(! v var
|
|
Jerry James |
17aa174 |
(! f formula
|
|
Jerry James |
17aa174 |
(! C clause
|
|
Jerry James |
17aa174 |
(! r (atom v f)
|
|
Jerry James |
17aa174 |
(! u (! o (th_holds (not f))
|
|
Jerry James |
17aa174 |
(holds C))
|
|
Jerry James |
17aa174 |
(holds (clc (pos v) C))))))))
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
(declare contra
|
|
Jerry James |
17aa174 |
(! f formula
|
|
Jerry James |
17aa174 |
(! r1 (th_holds f)
|
|
Jerry James |
17aa174 |
(! r2 (th_holds (not f))
|
|
Jerry James |
17aa174 |
(holds cln)))))
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
(declare th_ast
|
|
Jerry James |
17aa174 |
(! f formula
|
|
Jerry James |
17aa174 |
(! u (! o (th_holds f)
|
|
Jerry James |
17aa174 |
(holds cln))
|
|
Jerry James |
17aa174 |
(th_holds (not f)))))
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
(declare th_asf
|
|
Jerry James |
17aa174 |
(! f formula
|
|
Jerry James |
17aa174 |
(! u (! o (th_holds (not f))
|
|
Jerry James |
17aa174 |
(holds cln))
|
|
Jerry James |
17aa174 |
(th_holds f))))
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
(declare lem
|
|
Jerry James |
17aa174 |
(! f formula
|
|
Jerry James |
17aa174 |
(! v var
|
|
Jerry James |
17aa174 |
(! a (atom v f)
|
|
Jerry James |
17aa174 |
(holds (clc (pos v) (clc (neg v) cln)))))))
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
Jerry James |
17aa174 |
;
|
|
Jerry James |
17aa174 |
; Theory of Equality and Congruence Closure
|
|
Jerry James |
17aa174 |
;
|
|
Jerry James |
17aa174 |
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
(declare refl
|
|
Jerry James |
17aa174 |
(! s sort
|
|
Jerry James |
17aa174 |
(! t (term s)
|
|
Jerry James |
17aa174 |
(th_holds (= s t t)))))
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
(declare symm (! s sort
|
|
Jerry James |
17aa174 |
(! x (term s)
|
|
Jerry James |
17aa174 |
(! y (term s)
|
|
Jerry James |
17aa174 |
(! u (th_holds (= _ x y))
|
|
Jerry James |
17aa174 |
(th_holds (= _ y x)))))))
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
(declare trans (! s sort
|
|
Jerry James |
17aa174 |
(! x (term s)
|
|
Jerry James |
17aa174 |
(! y (term s)
|
|
Jerry James |
17aa174 |
(! z (term s)
|
|
Jerry James |
17aa174 |
(! u (th_holds (= _ x y))
|
|
Jerry James |
17aa174 |
(! u (th_holds (= _ y z))
|
|
Jerry James |
17aa174 |
(th_holds (= _ x z)))))))))
|
|
Jerry James |
17aa174 |
|
|
Jerry James |
17aa174 |
(declare cong (! s1 sort
|
|
Jerry James |
17aa174 |
(! s2 sort
|
|
Jerry James |
17aa174 |
(! a1 (term (arrow s1 s2))
|
|
Jerry James |
17aa174 |
(! b1 (term (arrow s1 s2))
|
|
Jerry James |
17aa174 |
(! a2 (term s1)
|
|
Jerry James |
17aa174 |
(! b2 (term s1)
|
|
Jerry James |
17aa174 |
(! u1 (th_holds (= _ a1 b1))
|
|
Jerry James |
17aa174 |
(! u2 (th_holds (= _ a2 b2))
|
|
Jerry James |
17aa174 |
(th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2))))))))))))
|
|
Jerry James |
17aa174 |
|