blob: c454a6dfe5eb682fb3caca11fbf30094f6b7e17e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
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))
)))))))))))))))))))))))))))
|
