36 *) |
36 *) |
37 |
37 |
38 writeln"Pelletier's examples"; |
38 writeln"Pelletier's examples"; |
39 (*1*) |
39 (*1*) |
40 goal FOL.thy "(P-->Q) <-> (~Q --> ~P)"; |
40 goal FOL.thy "(P-->Q) <-> (~Q --> ~P)"; |
41 by (fast_tac FOL_cs 1); |
41 by (Fast_tac 1); |
42 result(); |
42 result(); |
43 |
43 |
44 (*2*) |
44 (*2*) |
45 goal FOL.thy "~ ~ P <-> P"; |
45 goal FOL.thy "~ ~ P <-> P"; |
46 by (fast_tac FOL_cs 1); |
46 by (Fast_tac 1); |
47 result(); |
47 result(); |
48 |
48 |
49 (*3*) |
49 (*3*) |
50 goal FOL.thy "~(P-->Q) --> (Q-->P)"; |
50 goal FOL.thy "~(P-->Q) --> (Q-->P)"; |
51 by (fast_tac FOL_cs 1); |
51 by (Fast_tac 1); |
52 result(); |
52 result(); |
53 |
53 |
54 (*4*) |
54 (*4*) |
55 goal FOL.thy "(~P-->Q) <-> (~Q --> P)"; |
55 goal FOL.thy "(~P-->Q) <-> (~Q --> P)"; |
56 by (fast_tac FOL_cs 1); |
56 by (Fast_tac 1); |
57 result(); |
57 result(); |
58 |
58 |
59 (*5*) |
59 (*5*) |
60 goal FOL.thy "((P|Q)-->(P|R)) --> (P|(Q-->R))"; |
60 goal FOL.thy "((P|Q)-->(P|R)) --> (P|(Q-->R))"; |
61 by (fast_tac FOL_cs 1); |
61 by (Fast_tac 1); |
62 result(); |
62 result(); |
63 |
63 |
64 (*6*) |
64 (*6*) |
65 goal FOL.thy "P | ~ P"; |
65 goal FOL.thy "P | ~ P"; |
66 by (fast_tac FOL_cs 1); |
66 by (Fast_tac 1); |
67 result(); |
67 result(); |
68 |
68 |
69 (*7*) |
69 (*7*) |
70 goal FOL.thy "P | ~ ~ ~ P"; |
70 goal FOL.thy "P | ~ ~ ~ P"; |
71 by (fast_tac FOL_cs 1); |
71 by (Fast_tac 1); |
72 result(); |
72 result(); |
73 |
73 |
74 (*8. Peirce's law*) |
74 (*8. Peirce's law*) |
75 goal FOL.thy "((P-->Q) --> P) --> P"; |
75 goal FOL.thy "((P-->Q) --> P) --> P"; |
76 by (fast_tac FOL_cs 1); |
76 by (Fast_tac 1); |
77 result(); |
77 result(); |
78 |
78 |
79 (*9*) |
79 (*9*) |
80 goal FOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"; |
80 goal FOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"; |
81 by (fast_tac FOL_cs 1); |
81 by (Fast_tac 1); |
82 result(); |
82 result(); |
83 |
83 |
84 (*10*) |
84 (*10*) |
85 goal FOL.thy "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"; |
85 goal FOL.thy "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"; |
86 by (fast_tac FOL_cs 1); |
86 by (Fast_tac 1); |
87 result(); |
87 result(); |
88 |
88 |
89 (*11. Proved in each direction (incorrectly, says Pelletier!!) *) |
89 (*11. Proved in each direction (incorrectly, says Pelletier!!) *) |
90 goal FOL.thy "P<->P"; |
90 goal FOL.thy "P<->P"; |
91 by (fast_tac FOL_cs 1); |
91 by (Fast_tac 1); |
92 result(); |
92 result(); |
93 |
93 |
94 (*12. "Dijkstra's law"*) |
94 (*12. "Dijkstra's law"*) |
95 goal FOL.thy "((P <-> Q) <-> R) <-> (P <-> (Q <-> R))"; |
95 goal FOL.thy "((P <-> Q) <-> R) <-> (P <-> (Q <-> R))"; |
96 by (fast_tac FOL_cs 1); |
96 by (Fast_tac 1); |
97 result(); |
97 result(); |
98 |
98 |
99 (*13. Distributive law*) |
99 (*13. Distributive law*) |
100 goal FOL.thy "P | (Q & R) <-> (P | Q) & (P | R)"; |
100 goal FOL.thy "P | (Q & R) <-> (P | Q) & (P | R)"; |
101 by (fast_tac FOL_cs 1); |
101 by (Fast_tac 1); |
102 result(); |
102 result(); |
103 |
103 |
104 (*14*) |
104 (*14*) |
105 goal FOL.thy "(P <-> Q) <-> ((Q | ~P) & (~Q|P))"; |
105 goal FOL.thy "(P <-> Q) <-> ((Q | ~P) & (~Q|P))"; |
106 by (fast_tac FOL_cs 1); |
106 by (Fast_tac 1); |
107 result(); |
107 result(); |
108 |
108 |
109 (*15*) |
109 (*15*) |
110 goal FOL.thy "(P --> Q) <-> (~P | Q)"; |
110 goal FOL.thy "(P --> Q) <-> (~P | Q)"; |
111 by (fast_tac FOL_cs 1); |
111 by (Fast_tac 1); |
112 result(); |
112 result(); |
113 |
113 |
114 (*16*) |
114 (*16*) |
115 goal FOL.thy "(P-->Q) | (Q-->P)"; |
115 goal FOL.thy "(P-->Q) | (Q-->P)"; |
116 by (fast_tac FOL_cs 1); |
116 by (Fast_tac 1); |
117 result(); |
117 result(); |
118 |
118 |
119 (*17*) |
119 (*17*) |
120 goal FOL.thy "((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"; |
120 goal FOL.thy "((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"; |
121 by (fast_tac FOL_cs 1); |
121 by (Fast_tac 1); |
122 result(); |
122 result(); |
123 |
123 |
124 writeln"Classical Logic: examples with quantifiers"; |
124 writeln"Classical Logic: examples with quantifiers"; |
125 |
125 |
126 goal FOL.thy "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"; |
126 goal FOL.thy "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"; |
127 by (fast_tac FOL_cs 1); |
127 by (Fast_tac 1); |
128 result(); |
128 result(); |
129 |
129 |
130 goal FOL.thy "(EX x. P-->Q(x)) <-> (P --> (EX x.Q(x)))"; |
130 goal FOL.thy "(EX x. P-->Q(x)) <-> (P --> (EX x.Q(x)))"; |
131 by (fast_tac FOL_cs 1); |
131 by (Fast_tac 1); |
132 result(); |
132 result(); |
133 |
133 |
134 goal FOL.thy "(EX x.P(x)-->Q) <-> (ALL x.P(x)) --> Q"; |
134 goal FOL.thy "(EX x.P(x)-->Q) <-> (ALL x.P(x)) --> Q"; |
135 by (fast_tac FOL_cs 1); |
135 by (Fast_tac 1); |
136 result(); |
136 result(); |
137 |
137 |
138 goal FOL.thy "(ALL x.P(x)) | Q <-> (ALL x. P(x) | Q)"; |
138 goal FOL.thy "(ALL x.P(x)) | Q <-> (ALL x. P(x) | Q)"; |
139 by (fast_tac FOL_cs 1); |
139 by (Fast_tac 1); |
140 result(); |
140 result(); |
141 |
141 |
142 (*Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux, |
142 (*Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux, |
143 JAR 10 (265-281), 1993. Proof is trivial!*) |
143 JAR 10 (265-281), 1993. Proof is trivial!*) |
144 goal FOL.thy |
144 goal FOL.thy |
145 "~ ((EX x.~P(x)) & ((EX x.P(x)) | (EX x.P(x) & Q(x))) & ~ (EX x.P(x)))"; |
145 "~ ((EX x.~P(x)) & ((EX x.P(x)) | (EX x.P(x) & Q(x))) & ~ (EX x.P(x)))"; |
146 by (fast_tac FOL_cs 1); |
146 by (Fast_tac 1); |
147 result(); |
147 result(); |
148 |
148 |
149 writeln"Problems requiring quantifier duplication"; |
149 writeln"Problems requiring quantifier duplication"; |
150 |
150 |
151 (*Needs multiple instantiation of ALL.*) |
151 (*Needs multiple instantiation of ALL.*) |
152 goal FOL.thy "(ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"; |
152 goal FOL.thy "(ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"; |
153 by (deepen_tac FOL_cs 0 1); |
153 by (Deepen_tac 0 1); |
154 result(); |
154 result(); |
155 |
155 |
156 (*Needs double instantiation of the quantifier*) |
156 (*Needs double instantiation of the quantifier*) |
157 goal FOL.thy "EX x. P(x) --> P(a) & P(b)"; |
157 goal FOL.thy "EX x. P(x) --> P(a) & P(b)"; |
158 by (deepen_tac FOL_cs 0 1); |
158 by (Deepen_tac 0 1); |
159 result(); |
159 result(); |
160 |
160 |
161 goal FOL.thy "EX z. P(z) --> (ALL x. P(x))"; |
161 goal FOL.thy "EX z. P(z) --> (ALL x. P(x))"; |
162 by (deepen_tac FOL_cs 0 1); |
162 by (Deepen_tac 0 1); |
163 result(); |
163 result(); |
164 |
164 |
165 goal FOL.thy "EX x. (EX y. P(y)) --> P(x)"; |
165 goal FOL.thy "EX x. (EX y. P(y)) --> P(x)"; |
166 by (deepen_tac FOL_cs 0 1); |
166 by (Deepen_tac 0 1); |
167 result(); |
167 result(); |
168 |
168 |
169 (*V. Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23. NOT PROVED*) |
169 (*V. Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23. NOT PROVED*) |
170 goal FOL.thy "EX x x'. ALL y. EX z z'. \ |
170 goal FOL.thy "EX x x'. ALL y. EX z z'. \ |
171 \ (~P(y,y) | P(x,x) | ~S(z,x)) & \ |
171 \ (~P(y,y) | P(x,x) | ~S(z,x)) & \ |
174 |
174 |
175 writeln"Hard examples with quantifiers"; |
175 writeln"Hard examples with quantifiers"; |
176 |
176 |
177 writeln"Problem 18"; |
177 writeln"Problem 18"; |
178 goal FOL.thy "EX y. ALL x. P(y)-->P(x)"; |
178 goal FOL.thy "EX y. ALL x. P(y)-->P(x)"; |
179 by (deepen_tac FOL_cs 0 1); |
179 by (Deepen_tac 0 1); |
180 result(); |
180 result(); |
181 |
181 |
182 writeln"Problem 19"; |
182 writeln"Problem 19"; |
183 goal FOL.thy "EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"; |
183 goal FOL.thy "EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"; |
184 by (deepen_tac FOL_cs 0 1); |
184 by (Deepen_tac 0 1); |
185 result(); |
185 result(); |
186 |
186 |
187 writeln"Problem 20"; |
187 writeln"Problem 20"; |
188 goal FOL.thy "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) \ |
188 goal FOL.thy "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) \ |
189 \ --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"; |
189 \ --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"; |
190 by (fast_tac FOL_cs 1); |
190 by (Fast_tac 1); |
191 result(); |
191 result(); |
192 |
192 |
193 writeln"Problem 21"; |
193 writeln"Problem 21"; |
194 goal FOL.thy "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))"; |
194 goal FOL.thy "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))"; |
195 by (deepen_tac FOL_cs 0 1); |
195 by (Deepen_tac 0 1); |
196 result(); |
196 result(); |
197 |
197 |
198 writeln"Problem 22"; |
198 writeln"Problem 22"; |
199 goal FOL.thy "(ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"; |
199 goal FOL.thy "(ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"; |
200 by (fast_tac FOL_cs 1); |
200 by (Fast_tac 1); |
201 result(); |
201 result(); |
202 |
202 |
203 writeln"Problem 23"; |
203 writeln"Problem 23"; |
204 goal FOL.thy "(ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))"; |
204 goal FOL.thy "(ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))"; |
205 by (best_tac FOL_cs 1); |
205 by (Best_tac 1); |
206 result(); |
206 result(); |
207 |
207 |
208 writeln"Problem 24"; |
208 writeln"Problem 24"; |
209 goal FOL.thy "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \ |
209 goal FOL.thy "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \ |
210 \ ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x)) \ |
210 \ ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x)) \ |
211 \ --> (EX x. P(x)&R(x))"; |
211 \ --> (EX x. P(x)&R(x))"; |
212 by (fast_tac FOL_cs 1); |
212 by (Fast_tac 1); |
213 result(); |
213 result(); |
214 |
214 |
215 writeln"Problem 25"; |
215 writeln"Problem 25"; |
216 goal FOL.thy "(EX x. P(x)) & \ |
216 goal FOL.thy "(EX x. P(x)) & \ |
217 \ (ALL x. L(x) --> ~ (M(x) & R(x))) & \ |
217 \ (ALL x. L(x) --> ~ (M(x) & R(x))) & \ |
218 \ (ALL x. P(x) --> (M(x) & L(x))) & \ |
218 \ (ALL x. P(x) --> (M(x) & L(x))) & \ |
219 \ ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) \ |
219 \ ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) \ |
220 \ --> (EX x. Q(x)&P(x))"; |
220 \ --> (EX x. Q(x)&P(x))"; |
221 by (best_tac FOL_cs 1); |
221 by (Best_tac 1); |
222 result(); |
222 result(); |
223 |
223 |
224 writeln"Problem 26"; |
224 writeln"Problem 26"; |
225 goal FOL.thy "((EX x. p(x)) <-> (EX x. q(x))) & \ |
225 goal FOL.thy "((EX x. p(x)) <-> (EX x. q(x))) & \ |
226 \ (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y))) \ |
226 \ (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y))) \ |
227 \ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"; |
227 \ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"; |
228 by (fast_tac FOL_cs 1); |
228 by (Fast_tac 1); |
229 result(); |
229 result(); |
230 |
230 |
231 writeln"Problem 27"; |
231 writeln"Problem 27"; |
232 goal FOL.thy "(EX x. P(x) & ~Q(x)) & \ |
232 goal FOL.thy "(EX x. P(x) & ~Q(x)) & \ |
233 \ (ALL x. P(x) --> R(x)) & \ |
233 \ (ALL x. P(x) --> R(x)) & \ |
234 \ (ALL x. M(x) & L(x) --> P(x)) & \ |
234 \ (ALL x. M(x) & L(x) --> P(x)) & \ |
235 \ ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) \ |
235 \ ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) \ |
236 \ --> (ALL x. M(x) --> ~L(x))"; |
236 \ --> (ALL x. M(x) --> ~L(x))"; |
237 by (fast_tac FOL_cs 1); |
237 by (Fast_tac 1); |
238 result(); |
238 result(); |
239 |
239 |
240 writeln"Problem 28. AMENDED"; |
240 writeln"Problem 28. AMENDED"; |
241 goal FOL.thy "(ALL x. P(x) --> (ALL x. Q(x))) & \ |
241 goal FOL.thy "(ALL x. P(x) --> (ALL x. Q(x))) & \ |
242 \ ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & \ |
242 \ ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & \ |
243 \ ((EX x.S(x)) --> (ALL x. L(x) --> M(x))) \ |
243 \ ((EX x.S(x)) --> (ALL x. L(x) --> M(x))) \ |
244 \ --> (ALL x. P(x) & L(x) --> M(x))"; |
244 \ --> (ALL x. P(x) & L(x) --> M(x))"; |
245 by (fast_tac FOL_cs 1); |
245 by (Fast_tac 1); |
246 result(); |
246 result(); |
247 |
247 |
248 writeln"Problem 29. Essentially the same as Principia Mathematica *11.71"; |
248 writeln"Problem 29. Essentially the same as Principia Mathematica *11.71"; |
249 goal FOL.thy "(EX x. P(x)) & (EX y. Q(y)) \ |
249 goal FOL.thy "(EX x. P(x)) & (EX y. Q(y)) \ |
250 \ --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <-> \ |
250 \ --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <-> \ |
251 \ (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"; |
251 \ (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"; |
252 by (fast_tac FOL_cs 1); |
252 by (Fast_tac 1); |
253 result(); |
253 result(); |
254 |
254 |
255 writeln"Problem 30"; |
255 writeln"Problem 30"; |
256 goal FOL.thy "(ALL x. P(x) | Q(x) --> ~ R(x)) & \ |
256 goal FOL.thy "(ALL x. P(x) | Q(x) --> ~ R(x)) & \ |
257 \ (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) \ |
257 \ (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) \ |
258 \ --> (ALL x. S(x))"; |
258 \ --> (ALL x. S(x))"; |
259 by (fast_tac FOL_cs 1); |
259 by (Fast_tac 1); |
260 result(); |
260 result(); |
261 |
261 |
262 writeln"Problem 31"; |
262 writeln"Problem 31"; |
263 goal FOL.thy "~(EX x.P(x) & (Q(x) | R(x))) & \ |
263 goal FOL.thy "~(EX x.P(x) & (Q(x) | R(x))) & \ |
264 \ (EX x. L(x) & P(x)) & \ |
264 \ (EX x. L(x) & P(x)) & \ |
265 \ (ALL x. ~ R(x) --> M(x)) \ |
265 \ (ALL x. ~ R(x) --> M(x)) \ |
266 \ --> (EX x. L(x) & M(x))"; |
266 \ --> (EX x. L(x) & M(x))"; |
267 by (fast_tac FOL_cs 1); |
267 by (Fast_tac 1); |
268 result(); |
268 result(); |
269 |
269 |
270 writeln"Problem 32"; |
270 writeln"Problem 32"; |
271 goal FOL.thy "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \ |
271 goal FOL.thy "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \ |
272 \ (ALL x. S(x) & R(x) --> L(x)) & \ |
272 \ (ALL x. S(x) & R(x) --> L(x)) & \ |
273 \ (ALL x. M(x) --> R(x)) \ |
273 \ (ALL x. M(x) --> R(x)) \ |
274 \ --> (ALL x. P(x) & M(x) --> L(x))"; |
274 \ --> (ALL x. P(x) & M(x) --> L(x))"; |
275 by (best_tac FOL_cs 1); |
275 by (Best_tac 1); |
276 result(); |
276 result(); |
277 |
277 |
278 writeln"Problem 33"; |
278 writeln"Problem 33"; |
279 goal FOL.thy "(ALL x. P(a) & (P(x)-->P(b))-->P(c)) <-> \ |
279 goal FOL.thy "(ALL x. P(a) & (P(x)-->P(b))-->P(c)) <-> \ |
280 \ (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"; |
280 \ (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"; |
281 by (best_tac FOL_cs 1); |
281 by (Best_tac 1); |
282 result(); |
282 result(); |
283 |
283 |
284 writeln"Problem 34 AMENDED (TWICE!!)"; |
284 writeln"Problem 34 AMENDED (TWICE!!)"; |
285 (*Andrews's challenge*) |
285 (*Andrews's challenge*) |
286 goal FOL.thy "((EX x. ALL y. p(x) <-> p(y)) <-> \ |
286 goal FOL.thy "((EX x. ALL y. p(x) <-> p(y)) <-> \ |
287 \ ((EX x. q(x)) <-> (ALL y. p(y)))) <-> \ |
287 \ ((EX x. q(x)) <-> (ALL y. p(y)))) <-> \ |
288 \ ((EX x. ALL y. q(x) <-> q(y)) <-> \ |
288 \ ((EX x. ALL y. q(x) <-> q(y)) <-> \ |
289 \ ((EX x. p(x)) <-> (ALL y. q(y))))"; |
289 \ ((EX x. p(x)) <-> (ALL y. q(y))))"; |
290 by (deepen_tac FOL_cs 0 1); |
290 by (Deepen_tac 0 1); |
291 result(); |
291 result(); |
292 |
292 |
293 writeln"Problem 35"; |
293 writeln"Problem 35"; |
294 goal FOL.thy "EX x y. P(x,y) --> (ALL u v. P(u,v))"; |
294 goal FOL.thy "EX x y. P(x,y) --> (ALL u v. P(u,v))"; |
295 by (mini_tac 1); |
295 by (mini_tac 1); |
296 by (fast_tac FOL_cs 1); |
296 by (Fast_tac 1); |
297 (*Without miniscope, would have to use deepen_tac; would be slower*) |
297 (*Without miniscope, would have to use deepen_tac; would be slower*) |
298 result(); |
298 result(); |
299 |
299 |
300 writeln"Problem 36"; |
300 writeln"Problem 36"; |
301 goal FOL.thy |
301 goal FOL.thy |
302 "(ALL x. EX y. J(x,y)) & \ |
302 "(ALL x. EX y. J(x,y)) & \ |
303 \ (ALL x. EX y. G(x,y)) & \ |
303 \ (ALL x. EX y. G(x,y)) & \ |
304 \ (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z))) \ |
304 \ (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z))) \ |
305 \ --> (ALL x. EX y. H(x,y))"; |
305 \ --> (ALL x. EX y. H(x,y))"; |
306 by (fast_tac FOL_cs 1); |
306 by (Fast_tac 1); |
307 result(); |
307 result(); |
308 |
308 |
309 writeln"Problem 37"; |
309 writeln"Problem 37"; |
310 goal FOL.thy "(ALL z. EX w. ALL x. EX y. \ |
310 goal FOL.thy "(ALL z. EX w. ALL x. EX y. \ |
311 \ (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \ |
311 \ (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \ |
312 \ (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \ |
312 \ (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \ |
313 \ ((EX x y. Q(x,y)) --> (ALL x. R(x,x))) \ |
313 \ ((EX x y. Q(x,y)) --> (ALL x. R(x,x))) \ |
314 \ --> (ALL x. EX y. R(x,y))"; |
314 \ --> (ALL x. EX y. R(x,y))"; |
315 by (fast_tac FOL_cs 1); |
315 by (Fast_tac 1); |
316 result(); |
316 result(); |
317 |
317 |
318 writeln"Problem 38"; |
318 writeln"Problem 38"; |
319 goal FOL.thy |
319 goal FOL.thy |
320 "(ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) --> \ |
320 "(ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) --> \ |
321 \ (EX z. EX w. p(z) & r(x,w) & r(w,z))) <-> \ |
321 \ (EX z. EX w. p(z) & r(x,w) & r(w,z))) <-> \ |
322 \ (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) & \ |
322 \ (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) & \ |
323 \ (~p(a) | ~(EX y. p(y) & r(x,y)) | \ |
323 \ (~p(a) | ~(EX y. p(y) & r(x,y)) | \ |
324 \ (EX z. EX w. p(z) & r(x,w) & r(w,z))))"; |
324 \ (EX z. EX w. p(z) & r(x,w) & r(w,z))))"; |
325 by (deepen_tac FOL_cs 0 1); (*beats fast_tac!*) |
325 by (Deepen_tac 0 1); (*beats fast_tac!*) |
326 result(); |
326 result(); |
327 |
327 |
328 writeln"Problem 39"; |
328 writeln"Problem 39"; |
329 goal FOL.thy "~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"; |
329 goal FOL.thy "~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"; |
330 by (fast_tac FOL_cs 1); |
330 by (Fast_tac 1); |
331 result(); |
331 result(); |
332 |
332 |
333 writeln"Problem 40. AMENDED"; |
333 writeln"Problem 40. AMENDED"; |
334 goal FOL.thy "(EX y. ALL x. F(x,y) <-> F(x,x)) --> \ |
334 goal FOL.thy "(EX y. ALL x. F(x,y) <-> F(x,x)) --> \ |
335 \ ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"; |
335 \ ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"; |
336 by (fast_tac FOL_cs 1); |
336 by (Fast_tac 1); |
337 result(); |
337 result(); |
338 |
338 |
339 writeln"Problem 41"; |
339 writeln"Problem 41"; |
340 goal FOL.thy "(ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x)) \ |
340 goal FOL.thy "(ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x)) \ |
341 \ --> ~ (EX z. ALL x. f(x,z))"; |
341 \ --> ~ (EX z. ALL x. f(x,z))"; |
342 by (fast_tac FOL_cs 1); |
342 by (Fast_tac 1); |
343 result(); |
343 result(); |
344 |
344 |
345 writeln"Problem 42"; |
345 writeln"Problem 42"; |
346 goal FOL.thy "~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))"; |
346 goal FOL.thy "~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))"; |
347 by (deepen_tac FOL_cs 0 1); |
347 by (Deepen_tac 0 1); |
348 result(); |
348 result(); |
349 |
349 |
350 writeln"Problem 43"; |
350 writeln"Problem 43"; |
351 goal FOL.thy "(ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y))) \ |
351 goal FOL.thy "(ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y))) \ |
352 \ --> (ALL x. ALL y. q(x,y) <-> q(y,x))"; |
352 \ --> (ALL x. ALL y. q(x,y) <-> q(y,x))"; |
353 by (mini_tac 1); |
353 by (Auto_tac()); |
354 by (deepen_tac FOL_cs 5 1); |
354 (*The proof above cheats by using rewriting! A purely logical proof is |
355 (*Faster alternative proof! |
355 by (mini_tac 1 THEN Deepen_tac 5 1); |
356 by (asm_simp_tac FOL_ss 1); by (fast_tac FOL_cs 1); |
|
357 Can use just deepen_tac but it requires 253 secs?!? |
356 Can use just deepen_tac but it requires 253 secs?!? |
358 by (deepen_tac FOL_cs 0 1); |
357 by (Deepen_tac 0 1); |
359 *) |
358 *) |
360 result(); |
359 result(); |
361 |
360 |
362 writeln"Problem 44"; |
361 writeln"Problem 44"; |
363 goal FOL.thy "(ALL x. f(x) --> \ |
362 goal FOL.thy "(ALL x. f(x) --> \ |
364 \ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \ |
363 \ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \ |
365 \ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \ |
364 \ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \ |
366 \ --> (EX x. j(x) & ~f(x))"; |
365 \ --> (EX x. j(x) & ~f(x))"; |
367 by (fast_tac FOL_cs 1); |
366 by (Fast_tac 1); |
368 result(); |
367 result(); |
369 |
368 |
370 writeln"Problem 45"; |
369 writeln"Problem 45"; |
371 goal FOL.thy "(ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y)) \ |
370 goal FOL.thy "(ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y)) \ |
372 \ --> (ALL y. g(y) & h(x,y) --> k(y))) & \ |
371 \ --> (ALL y. g(y) & h(x,y) --> k(y))) & \ |
373 \ ~ (EX y. l(y) & k(y)) & \ |
372 \ ~ (EX y. l(y) & k(y)) & \ |
374 \ (EX x. f(x) & (ALL y. h(x,y) --> l(y)) \ |
373 \ (EX x. f(x) & (ALL y. h(x,y) --> l(y)) \ |
375 \ & (ALL y. g(y) & h(x,y) --> j(x,y))) \ |
374 \ & (ALL y. g(y) & h(x,y) --> j(x,y))) \ |
376 \ --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))"; |
375 \ --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))"; |
377 by (best_tac FOL_cs 1); |
376 by (Best_tac 1); |
378 result(); |
377 result(); |
379 |
378 |
380 |
379 |
381 writeln"Problems (mainly) involving equality or functions"; |
380 writeln"Problems (mainly) involving equality or functions"; |
382 |
381 |
383 writeln"Problem 48"; |
382 writeln"Problem 48"; |
384 goal FOL.thy "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"; |
383 goal FOL.thy "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"; |
385 by (fast_tac FOL_cs 1); |
384 by (Fast_tac 1); |
386 result(); |
385 result(); |
387 |
386 |
388 writeln"Problem 49 NOT PROVED AUTOMATICALLY"; |
387 writeln"Problem 49 NOT PROVED AUTOMATICALLY"; |
389 (*Hard because it involves substitution for Vars; |
388 (*Hard because it involves substitution for Vars; |
390 the type constraint ensures that x,y,z have the same type as a,b,u. *) |
389 the type constraint ensures that x,y,z have the same type as a,b,u. *) |
391 goal FOL.thy "(EX x y::'a. ALL z. z=x | z=y) & P(a) & P(b) & a~=b \ |
390 goal FOL.thy "(EX x y::'a. ALL z. z=x | z=y) & P(a) & P(b) & a~=b \ |
392 \ --> (ALL u::'a.P(u))"; |
391 \ --> (ALL u::'a.P(u))"; |
393 by (safe_tac FOL_cs); |
392 by (Step_tac 1); |
394 by (res_inst_tac [("x","a")] allE 1); |
393 by (res_inst_tac [("x","a")] allE 1); |
395 by (assume_tac 1); |
394 by (assume_tac 1); |
396 by (res_inst_tac [("x","b")] allE 1); |
395 by (res_inst_tac [("x","b")] allE 1); |
397 by (assume_tac 1); |
396 by (assume_tac 1); |
398 by (fast_tac FOL_cs 1); |
397 by (Fast_tac 1); |
399 result(); |
398 result(); |
400 |
399 |
401 writeln"Problem 50"; |
400 writeln"Problem 50"; |
402 (*What has this to do with equality?*) |
401 (*What has this to do with equality?*) |
403 goal FOL.thy "(ALL x. P(a,x) | (ALL y.P(x,y))) --> (EX x. ALL y.P(x,y))"; |
402 goal FOL.thy "(ALL x. P(a,x) | (ALL y.P(x,y))) --> (EX x. ALL y.P(x,y))"; |
404 by (mini_tac 1); |
403 by (mini_tac 1); |
405 by (deepen_tac FOL_cs 0 1); |
404 by (Deepen_tac 0 1); |
406 result(); |
405 result(); |
407 |
406 |
408 writeln"Problem 51"; |
407 writeln"Problem 51"; |
409 goal FOL.thy |
408 goal FOL.thy |
410 "(EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> \ |
409 "(EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> \ |
411 \ (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"; |
410 \ (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"; |
412 by (fast_tac FOL_cs 1); |
411 by (Fast_tac 1); |
413 result(); |
412 result(); |
414 |
413 |
415 writeln"Problem 52"; |
414 writeln"Problem 52"; |
416 (*Almost the same as 51. *) |
415 (*Almost the same as 51. *) |
417 goal FOL.thy |
416 goal FOL.thy |
418 "(EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> \ |
417 "(EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> \ |
419 \ (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)"; |
418 \ (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)"; |
420 by (best_tac FOL_cs 1); |
419 by (Best_tac 1); |
421 result(); |
420 result(); |
422 |
421 |
423 writeln"Problem 55"; |
422 writeln"Problem 55"; |
424 |
423 |
425 (*Original, equational version by Len Schubert, via Pelletier *** NOT PROVED |
424 (*Original, equational version by Len Schubert, via Pelletier *** NOT PROVED |
454 \ (hates(agatha,agatha) & hates(agatha,charles)) & \ |
453 \ (hates(agatha,agatha) & hates(agatha,charles)) & \ |
455 \ (ALL x. lives(x) & ~richer(x,agatha) --> hates(butler,x)) & \ |
454 \ (ALL x. lives(x) & ~richer(x,agatha) --> hates(butler,x)) & \ |
456 \ (ALL x. hates(agatha,x) --> hates(butler,x)) & \ |
455 \ (ALL x. hates(agatha,x) --> hates(butler,x)) & \ |
457 \ (ALL x. ~hates(x,agatha) | ~hates(x,butler) | ~hates(x,charles)) --> \ |
456 \ (ALL x. ~hates(x,agatha) | ~hates(x,butler) | ~hates(x,charles)) --> \ |
458 \ killed(?who,agatha)"; |
457 \ killed(?who,agatha)"; |
459 by (fast_tac FOL_cs 1); |
458 by (Fast_tac 1); |
460 result(); |
459 result(); |
461 |
460 |
462 |
461 |
463 writeln"Problem 56"; |
462 writeln"Problem 56"; |
464 goal FOL.thy |
463 goal FOL.thy |
465 "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"; |
464 "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"; |
466 by (fast_tac FOL_cs 1); |
465 by (Fast_tac 1); |
467 result(); |
466 result(); |
468 |
467 |
469 writeln"Problem 57"; |
468 writeln"Problem 57"; |
470 goal FOL.thy |
469 goal FOL.thy |
471 "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \ |
470 "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \ |
472 \ (ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))"; |
471 \ (ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))"; |
473 by (fast_tac FOL_cs 1); |
472 by (Fast_tac 1); |
474 result(); |
473 result(); |
475 |
474 |
476 writeln"Problem 58 NOT PROVED AUTOMATICALLY"; |
475 writeln"Problem 58 NOT PROVED AUTOMATICALLY"; |
477 goal FOL.thy "(ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"; |
476 goal FOL.thy "(ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"; |
478 by (slow_tac (FOL_cs addEs [subst_context]) 1); |
477 by (slow_tac (!claset addEs [subst_context]) 1); |
479 result(); |
478 result(); |
480 |
479 |
481 writeln"Problem 59"; |
480 writeln"Problem 59"; |
482 goal FOL.thy "(ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"; |
481 goal FOL.thy "(ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"; |
483 by (deepen_tac FOL_cs 0 1); |
482 by (Deepen_tac 0 1); |
484 result(); |
483 result(); |
485 |
484 |
486 writeln"Problem 60"; |
485 writeln"Problem 60"; |
487 goal FOL.thy |
486 goal FOL.thy |
488 "ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"; |
487 "ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"; |
489 by (fast_tac FOL_cs 1); |
488 by (Fast_tac 1); |
490 result(); |
489 result(); |
491 |
490 |
492 writeln"Problem 62 as corrected in AAR newletter #31"; |
491 writeln"Problem 62 as corrected in AAR newletter #31"; |
493 goal FOL.thy |
492 goal FOL.thy |
494 "(ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x)))) <-> \ |
493 "(ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x)))) <-> \ |
495 \ (ALL x. (~p(a) | p(x) | p(f(f(x)))) & \ |
494 \ (ALL x. (~p(a) | p(x) | p(f(f(x)))) & \ |
496 \ (~p(a) | ~p(f(x)) | p(f(f(x)))))"; |
495 \ (~p(a) | ~p(f(x)) | p(f(f(x)))))"; |
497 by (fast_tac FOL_cs 1); |
496 by (Fast_tac 1); |
498 result(); |
497 result(); |
499 |
498 |
500 (*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.) |
499 (*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.) |
501 author U. Egly*) |
500 author U. Egly*) |
502 goal FOL.thy |
501 goal FOL.thy |