blob: 67ce3988a350c07ab2c7f4aff9a912949dab9f26 (
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
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; SMT syntax and semantics (not theory-specific)
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare formula type)
(declare th_holds (! f formula type))
; constants
(declare true formula)
(declare false formula)
; logical connectives
(declare not (! f formula formula))
(declare and (! f1 formula (! f2 formula formula)))
(declare or (! f1 formula (! f2 formula formula)))
(declare impl (! f1 formula (! f2 formula formula)))
(declare iff (! f1 formula (! f2 formula formula)))
(declare xor (! f1 formula (! f2 formula formula)))
(declare ifte (! b formula (! f1 formula (! f2 formula formula))))
; terms
(declare sort type) ; sort in the theory
(declare arrow (! s1 sort (! s2 sort sort))) ; function constructor
(declare term (! t sort type)) ; declared terms in formula
(declare apply (! s1 sort
(! s2 sort
(! t1 (term (arrow s1 s2))
(! t2 (term s1)
(term s2))))))
(declare ite (! s sort
(! f formula
(! t1 (term s)
(! t2 (term s)
(term s))))))
; let/flet
(declare let (! s sort
(! t (term s)
(! f (! v (term s) formula)
formula))))
(declare flet (! f1 formula
(! f2 (! v formula formula)
formula)))
; predicates
(declare = (! s sort
(! x (term s)
(! y (term s)
formula))))
; To avoid duplicating some of the rules (e.g., cong), we will view
; applications of predicates as terms of sort "Bool".
; Such terms can be injected as atomic formulas using "p_app".
(declare Bool sort) ; the special sort for predicates
(declare p_app (! x (term Bool) formula)) ; propositional application of term
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Examples
; an example of "(p1 or p2(0)) and t1=t2(1)"
;(! p1 (term Bool)
;(! p2 (term (arrow Int Bool))
;(! t1 (term Int)
;(! t2 (term (arrow Int Int))
;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0)))
; (= _ t1 (apply _ _ t2 1))))
; ...
; another example of "p3(a,b)"
;(! a (term Int)
;(! b (term Int)
;(! p3 (term (arrow Int (arrow Int Bool))) ; arrow is right assoc.
;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc.
; ...
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Natural deduction rules : used for CNF
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; contradiction
(declare contra
(! f formula
(! r1 (th_holds f)
(! r2 (th_holds (not f))
(th_holds false)))))
;; not not
(declare not_not_intro
(! f formula
(! u (th_holds f)
(th_holds (not (not f))))))
(declare not_not_elim
(! f formula
(! u (th_holds (not (not f)))
(th_holds f))))
;; or elimination
(declare or_elim_1
(! f1 formula
(! f2 formula
(! u1 (th_holds (not f1))
(! u2 (th_holds (or f1 f2))
(th_holds f2))))))
(declare or_elim_2
(! f1 formula
(! f2 formula
(! u1 (th_holds (not f2))
(! u2 (th_holds (or f1 f2))
(th_holds f1))))))
;; and elimination
(declare and_elim_1
(! f1 formula
(! f2 formula
(! u (th_holds (and f1 f2))
(th_holds f1)))))
(declare and_elim_2
(! f1 formula
(! f2 formula
(! u (th_holds (and f1 f2))
(th_holds f2)))))
;; not impl elimination
(declare not_impl_elim_1
(! f1 formula
(! f2 formula
(! u (th_holds (not (impl f1 f2)))
(th_holds f1)))))
(declare not_impl_elim_2
(! f1 formula
(! f2 formula
(! u (th_holds (not (impl f1 f2)))
(th_holds (not f2))))))
;; impl elimination
(declare impl_intro (! f1 formula
(! f2 formula
(! i1 (! u (th_holds f1)
(th_holds f2))
(th_holds (impl f1 f2))))))
(declare impl_elim
(! f1 formula
(! f2 formula
(! u1 (th_holds f1)
(! u2 (th_holds (impl f1 f2))
(th_holds f2))))))
;; iff elimination
(declare iff_elim_1
(! f1 formula
(! f2 formula
(! u1 (th_holds (iff f1 f2))
(th_holds (impl f1 f2))))))
(declare iff_elim_2
(! f1 formula
(! f2 formula
(! u1 (th_holds (iff f1 f2))
(th_holds (impl f2 f1))))))
(declare not_iff_elim_1
(! f1 formula
(! f2 formula
(! u1 (th_holds (not f1))
(! u2 (th_holds (not (iff f1 f2)))
(th_holds f2))))))
(declare not_iff_elim_2
(! f1 formula
(! f2 formula
(! u1 (th_holds f1)
(! u2 (th_holds (not (iff f1 f2)))
(th_holds (not f2)))))))
;; ite elimination
(declare ite_elim_1
(! a formula
(! b formula
(! c formula
(! u1 (th_holds a)
(! u2 (th_holds (ifte a b c))
(th_holds b)))))))
(declare ite_elim_2
(! a formula
(! b formula
(! c formula
(! u1 (th_holds (not a))
(! u2 (th_holds (ifte a b c))
(th_holds c)))))))
(declare ite_elim_3
(! a formula
(! b formula
(! c formula
(! u1 (th_holds (not b))
(! u2 (th_holds (ifte a b c))
(th_holds c)))))))
(declare ite_elim_2n
(! a formula
(! b formula
(! c formula
(! u1 (th_holds a)
(! u2 (th_holds (ifte (not a) b c))
(th_holds c)))))))
(declare not_ite_elim_1
(! a formula
(! b formula
(! c formula
(! u1 (th_holds a)
(! u2 (th_holds (not (ifte a b c)))
(th_holds (not b))))))))
(declare not_ite_elim_2
(! a formula
(! b formula
(! c formula
(! u1 (th_holds (not a))
(! u2 (th_holds (not (ifte a b c)))
(th_holds (not c))))))))
(declare not_ite_elim_3
(! a formula
(! b formula
(! c formula
(! u1 (th_holds b)
(! u2 (th_holds (not (ifte a b c)))
(th_holds (not c))))))))
(declare not_ite_elim_2n
(! a formula
(! b formula
(! c formula
(! u1 (th_holds a)
(! u2 (th_holds (not (ifte (not a) b c)))
(th_holds (not c))))))))
;; How to do CNF for disjunctions of theory literals.
;;
;; Given theory literals F1....Fn, and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))).
;;
;; We introduce atoms a1...an for literals F1...Fn, mapping them to boolean literals v1...vn.
;; Do this at the beginning of the proof:
;;
;; (decl_atom F1 (\ v1 (\ a1
;; (decl_atom F2 (\ v2 (\ a2
;; ....
;; (decl_atom Fn (\ vn (\ an
;;
;; Our input A is clausified by the following proof:
;;
;;(satlem _ _
;;(asf _ _ _ a1 (\ l1
;;(asf _ _ _ a2 (\ l2
;;...
;;(asf _ _ _ an (\ ln
;;(clausify_false
;;
;; (contra _
;; (or_elim_1 _ _ l{n-1}
;; ...
;; (or_elim_1 _ _ l2
;; (or_elim_1 _ _ l1 A))))) ln)
;;
;;))))))) (\ C
;;
;; We now have the free variable C, which should be the clause (v1 V ... V vn).
;;
;; We also need to consider the polarity of literals, say we have A of the form (th_holds (or (not F1) (or F2 (not F3)))).
;; Where necessary, we use "ast" instead of "asf", introduce negations by "not_not_intro" for pattern matching, and flip
;; the arguments of contra:
;;
;;(satlem _ _
;;(ast _ _ _ a1 (\ l1
;;(asf _ _ _ a2 (\ l2
;;(ast _ _ _ a3 (\ l3
;;(clausify_false
;;
;; (contra _ l3
;; (or_elim_1 _ _ l2
;; (or_elim_1 _ _ (not_not_intro l1) A))))
;;
;;))))))) (\ C
;;
;; C should be the clause (~v1 V v2 V ~v3 )
|
