141 by (Blast_tac 1); |
141 by (Blast_tac 1); |
142 result(); |
142 result(); |
143 |
143 |
144 (*Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux, |
144 (*Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux, |
145 JAR 10 (265-281), 1993. Proof is trivial!*) |
145 JAR 10 (265-281), 1993. Proof is trivial!*) |
146 Goal "~ ((EX x.~P(x)) & ((EX x. P(x)) | (EX x. P(x) & Q(x))) & ~ (EX x. P(x)))"; |
146 Goal "~((EX x.~P(x)) & ((EX x. P(x)) | (EX x. P(x) & Q(x))) & ~ (EX x. P(x)))"; |
147 by (Blast_tac 1); |
147 by (Blast_tac 1); |
148 result(); |
148 result(); |
149 |
149 |
150 writeln"Problems requiring quantifier duplication"; |
150 writeln"Problems requiring quantifier duplication"; |
151 |
151 |
214 by (Blast_tac 1); |
214 by (Blast_tac 1); |
215 result(); |
215 result(); |
216 |
216 |
217 writeln"Problem 24"; |
217 writeln"Problem 24"; |
218 Goal "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \ |
218 Goal "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \ |
219 \ (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x)) \ |
219 \ (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x)) \ |
220 \ --> (EX x. P(x)&R(x))"; |
220 \ --> (EX x. P(x)&R(x))"; |
221 by (Blast_tac 1); |
221 by (Blast_tac 1); |
222 result(); |
222 result(); |
223 |
223 |
224 writeln"Problem 25"; |
224 writeln"Problem 25"; |
225 Goal "(EX x. P(x)) & \ |
225 Goal "(EX x. P(x)) & \ |
226 \ (ALL x. L(x) --> ~ (M(x) & R(x))) & \ |
226 \ (ALL x. L(x) --> ~ (M(x) & R(x))) & \ |
227 \ (ALL x. P(x) --> (M(x) & L(x))) & \ |
227 \ (ALL x. P(x) --> (M(x) & L(x))) & \ |
228 \ ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) \ |
228 \ ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) \ |
229 \ --> (EX x. Q(x)&P(x))"; |
229 \ --> (EX x. Q(x)&P(x))"; |
230 by (Blast_tac 1); |
230 by (Blast_tac 1); |
231 result(); |
231 result(); |
232 |
232 |
233 writeln"Problem 26"; |
233 writeln"Problem 26"; |
237 by (Blast_tac 1); |
237 by (Blast_tac 1); |
238 result(); |
238 result(); |
239 |
239 |
240 writeln"Problem 27"; |
240 writeln"Problem 27"; |
241 Goal "(EX x. P(x) & ~Q(x)) & \ |
241 Goal "(EX x. P(x) & ~Q(x)) & \ |
242 \ (ALL x. P(x) --> R(x)) & \ |
242 \ (ALL x. P(x) --> R(x)) & \ |
243 \ (ALL x. M(x) & L(x) --> P(x)) & \ |
243 \ (ALL x. M(x) & L(x) --> P(x)) & \ |
244 \ ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) \ |
244 \ ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) \ |
245 \ --> (ALL x. M(x) --> ~L(x))"; |
245 \ --> (ALL x. M(x) --> ~L(x))"; |
246 by (Blast_tac 1); |
246 by (Blast_tac 1); |
247 result(); |
247 result(); |
248 |
248 |
249 writeln"Problem 28. AMENDED"; |
249 writeln"Problem 28. AMENDED"; |
250 Goal "(ALL x. P(x) --> (ALL x. Q(x))) & \ |
250 Goal "(ALL x. P(x) --> (ALL x. Q(x))) & \ |
276 by (Blast_tac 1); |
276 by (Blast_tac 1); |
277 result(); |
277 result(); |
278 |
278 |
279 writeln"Problem 32"; |
279 writeln"Problem 32"; |
280 Goal "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \ |
280 Goal "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \ |
281 \ (ALL x. S(x) & R(x) --> L(x)) & \ |
281 \ (ALL x. S(x) & R(x) --> L(x)) & \ |
282 \ (ALL x. M(x) --> R(x)) \ |
282 \ (ALL x. M(x) --> R(x)) \ |
283 \ --> (ALL x. P(x) & M(x) --> L(x))"; |
283 \ --> (ALL x. P(x) & M(x) --> L(x))"; |
284 by (Blast_tac 1); |
284 by (Blast_tac 1); |
285 result(); |
285 result(); |
286 |
286 |
287 writeln"Problem 33"; |
287 writeln"Problem 33"; |
288 Goal "(ALL x. P(a) & (P(x)-->P(b))-->P(c)) <-> \ |
288 Goal "(ALL x. P(a) & (P(x)-->P(b))-->P(c)) <-> \ |
289 \ (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"; |
289 \ (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"; |
290 by (Blast_tac 1); |
290 by (Blast_tac 1); |
291 result(); |
291 result(); |
292 |
292 |
293 writeln"Problem 34 AMENDED (TWICE!!)"; |
293 writeln"Problem 34 AMENDED (TWICE!!)"; |
294 (*Andrews's challenge*) |
294 (*Andrews's challenge*) |
295 Goal "((EX x. ALL y. p(x) <-> p(y)) <-> \ |
295 Goal "((EX x. ALL y. p(x) <-> p(y)) <-> \ |
296 \ ((EX x. q(x)) <-> (ALL y. p(y)))) <-> \ |
296 \ ((EX x. q(x)) <-> (ALL y. p(y)))) <-> \ |
297 \ ((EX x. ALL y. q(x) <-> q(y)) <-> \ |
297 \ ((EX x. ALL y. q(x) <-> q(y)) <-> \ |
298 \ ((EX x. p(x)) <-> (ALL y. q(y))))"; |
298 \ ((EX x. p(x)) <-> (ALL y. q(y))))"; |
299 by (Blast_tac 1); |
299 by (Blast_tac 1); |
300 result(); |
300 result(); |
301 |
301 |
302 writeln"Problem 35"; |
302 writeln"Problem 35"; |
303 Goal "EX x y. P(x,y) --> (ALL u v. P(u,v))"; |
303 Goal "EX x y. P(x,y) --> (ALL u v. P(u,v))"; |
313 result(); |
313 result(); |
314 |
314 |
315 writeln"Problem 37"; |
315 writeln"Problem 37"; |
316 Goal "(ALL z. EX w. ALL x. EX y. \ |
316 Goal "(ALL z. EX w. ALL x. EX y. \ |
317 \ (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \ |
317 \ (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \ |
318 \ (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \ |
318 \ (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \ |
319 \ ((EX x y. Q(x,y)) --> (ALL x. R(x,x))) \ |
319 \ ((EX x y. Q(x,y)) --> (ALL x. R(x,x))) \ |
320 \ --> (ALL x. EX y. R(x,y))"; |
320 \ --> (ALL x. EX y. R(x,y))"; |
321 by (Blast_tac 1); |
321 by (Blast_tac 1); |
322 result(); |
322 result(); |
323 |
323 |
324 writeln"Problem 38"; |
324 writeln"Problem 38"; |
325 Goal "(ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) --> \ |
325 Goal "(ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) --> \ |
326 \ (EX z. EX w. p(z) & r(x,w) & r(w,z))) <-> \ |
326 \ (EX z. EX w. p(z) & r(x,w) & r(w,z))) <-> \ |
327 \ (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) & \ |
327 \ (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) & \ |
328 \ (~p(a) | ~(EX y. p(y) & r(x,y)) | \ |
328 \ (~p(a) | ~(EX y. p(y) & r(x,y)) | \ |
329 \ (EX z. EX w. p(z) & r(x,w) & r(w,z))))"; |
329 \ (EX z. EX w. p(z) & r(x,w) & r(w,z))))"; |
330 by (Blast_tac 1); (*beats fast_tac!*) |
330 by (Blast_tac 1); (*beats fast_tac!*) |
331 result(); |
331 result(); |
332 |
332 |
333 writeln"Problem 39"; |
333 writeln"Problem 39"; |
361 by (mini_tac 1 THEN Deepen_tac 5 1); |
361 by (mini_tac 1 THEN Deepen_tac 5 1); |
362 *) |
362 *) |
363 result(); |
363 result(); |
364 |
364 |
365 writeln"Problem 44"; |
365 writeln"Problem 44"; |
366 Goal "(ALL x. f(x) --> \ |
366 Goal "(ALL x. f(x) --> (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \ |
367 \ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \ |
367 \ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \ |
368 \ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \ |
368 \ --> (EX x. j(x) & ~f(x))"; |
369 \ --> (EX x. j(x) & ~f(x))"; |
|
370 by (Blast_tac 1); |
369 by (Blast_tac 1); |
371 result(); |
370 result(); |
372 |
371 |
373 writeln"Problem 45"; |
372 writeln"Problem 45"; |
374 Goal "(ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y)) \ |
373 Goal "(ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y)) \ |
381 result(); |
380 result(); |
382 |
381 |
383 |
382 |
384 writeln"Problem 46"; |
383 writeln"Problem 46"; |
385 Goal "(ALL x. f(x) & (ALL y. f(y) & h(y,x) --> g(y)) --> g(x)) & \ |
384 Goal "(ALL x. f(x) & (ALL y. f(y) & h(y,x) --> g(y)) --> g(x)) & \ |
386 \ ((EX x. f(x) & ~g(x)) --> \ |
385 \ ((EX x. f(x) & ~g(x)) --> \ |
387 \ (EX x. f(x) & ~g(x) & (ALL y. f(y) & ~g(y) --> j(x,y)))) & \ |
386 \ (EX x. f(x) & ~g(x) & (ALL y. f(y) & ~g(y) --> j(x,y)))) & \ |
388 \ (ALL x y. f(x) & f(y) & h(x,y) --> ~j(y,x)) \ |
387 \ (ALL x y. f(x) & f(y) & h(x,y) --> ~j(y,x)) \ |
389 \ --> (ALL x. f(x) --> g(x))"; |
388 \ --> (ALL x. f(x) --> g(x))"; |
390 by (Blast_tac 1); |
389 by (Blast_tac 1); |
391 result(); |
390 result(); |
392 |
391 |
393 |
392 |
394 writeln"Problems (mainly) involving equality or functions"; |
393 writeln"Problems (mainly) involving equality or functions"; |
417 by (Blast_tac 1); |
416 by (Blast_tac 1); |
418 result(); |
417 result(); |
419 |
418 |
420 writeln"Problem 51"; |
419 writeln"Problem 51"; |
421 Goal "(EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> \ |
420 Goal "(EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> \ |
422 \ (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"; |
421 \ (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"; |
423 by (Blast_tac 1); |
422 by (Blast_tac 1); |
424 result(); |
423 result(); |
425 |
424 |
426 writeln"Problem 52"; |
425 writeln"Problem 52"; |
427 (*Almost the same as 51. *) |
426 (*Almost the same as 51. *) |
428 Goal "(EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> \ |
427 Goal "(EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> \ |
429 \ (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)"; |
428 \ (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)"; |
430 by (Blast_tac 1); |
429 by (Blast_tac 1); |
431 result(); |
430 result(); |
432 |
431 |
433 writeln"Problem 55"; |
432 writeln"Problem 55"; |
434 |
433 |
496 by (Blast_tac 1); |
495 by (Blast_tac 1); |
497 result(); |
496 result(); |
498 |
497 |
499 writeln"Problem 62 as corrected in JAR 18 (1997), page 135"; |
498 writeln"Problem 62 as corrected in JAR 18 (1997), page 135"; |
500 Goal "(ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x)))) <-> \ |
499 Goal "(ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x)))) <-> \ |
501 \ (ALL x. (~p(a) | p(x) | p(f(f(x)))) & \ |
500 \ (ALL x. (~p(a) | p(x) | p(f(f(x)))) & \ |
502 \ (~p(a) | ~p(f(x)) | p(f(f(x)))))"; |
501 \ (~p(a) | ~p(f(x)) | p(f(f(x)))))"; |
503 by (Blast_tac 1); |
502 by (Blast_tac 1); |
504 result(); |
503 result(); |
505 |
504 |
506 (*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531 |
505 (*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531 |
507 Fast_tac indeed copes!*) |
506 Fast_tac indeed copes!*) |
512 result(); |
511 result(); |
513 |
512 |
514 (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393. |
513 (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393. |
515 It does seem obvious!*) |
514 It does seem obvious!*) |
516 Goal "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \ |
515 Goal "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \ |
517 \ (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) & \ |
516 \ (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) & \ |
518 \ (ALL x. K(x) --> ~G(x)) --> (EX x. K(x) --> ~G(x))"; |
517 \ (ALL x. K(x) --> ~G(x)) --> (EX x. K(x) --> ~G(x))"; |
519 by (Fast_tac 1); |
518 by (Fast_tac 1); |
520 result(); |
519 result(); |
521 |
520 |
522 (*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.) |
521 (*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.) |
523 author U. Egly*) |
522 author U. Egly*) |