243 by (meson_tac 1); |
243 by (meson_tac 1); |
244 result(); |
244 result(); |
245 |
245 |
246 writeln"Classical Logic: examples with quantifiers"; |
246 writeln"Classical Logic: examples with quantifiers"; |
247 |
247 |
248 Goal "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))"; |
248 Goal "(\\<forall>x. P x & Q x) = ((\\<forall>x. P x) & (\\<forall>x. Q x))"; |
249 by (meson_tac 1); |
249 by (meson_tac 1); |
250 result(); |
250 result(); |
251 |
251 |
252 Goal "(? x. P --> Q x) = (P --> (? x. Q x))"; |
252 Goal "(\\<exists>x. P --> Q x) = (P --> (\\<exists>x. Q x))"; |
253 by (meson_tac 1); |
253 by (meson_tac 1); |
254 result(); |
254 result(); |
255 |
255 |
256 Goal "(? x. P x --> Q) = ((! x. P x) --> Q)"; |
256 Goal "(\\<exists>x. P x --> Q) = ((\\<forall>x. P x) --> Q)"; |
257 by (meson_tac 1); |
257 by (meson_tac 1); |
258 result(); |
258 result(); |
259 |
259 |
260 Goal "((! x. P x) | Q) = (! x. P x | Q)"; |
260 Goal "((\\<forall>x. P x) | Q) = (\\<forall>x. P x | Q)"; |
261 by (meson_tac 1); |
261 by (meson_tac 1); |
262 result(); |
262 result(); |
263 |
263 |
264 Goal "(! x. P x --> P(f x)) & P d --> P(f(f(f d)))"; |
264 Goal "(\\<forall>x. P x --> P(f x)) & P d --> P(f(f(f d)))"; |
265 by (meson_tac 1); |
265 by (meson_tac 1); |
266 result(); |
266 result(); |
267 |
267 |
268 (*Needs double instantiation of EXISTS*) |
268 (*Needs double instantiation of EXISTS*) |
269 Goal "? x. P x --> P a & P b"; |
269 Goal "\\<exists>x. P x --> P a & P b"; |
270 by (meson_tac 1); |
270 by (meson_tac 1); |
271 result(); |
271 result(); |
272 |
272 |
273 Goal "? z. P z --> (! x. P x)"; |
273 Goal "\\<exists>z. P z --> (\\<forall>x. P x)"; |
274 by (meson_tac 1); |
274 by (meson_tac 1); |
275 result(); |
275 result(); |
276 |
276 |
277 writeln"Hard examples with quantifiers"; |
277 writeln"Hard examples with quantifiers"; |
278 |
278 |
279 writeln"Problem 18"; |
279 writeln"Problem 18"; |
280 Goal "? y. ! x. P y --> P x"; |
280 Goal "\\<exists>y. \\<forall>x. P y --> P x"; |
281 by (meson_tac 1); |
281 by (meson_tac 1); |
282 result(); |
282 result(); |
283 |
283 |
284 writeln"Problem 19"; |
284 writeln"Problem 19"; |
285 Goal "? x. ! y z. (P y --> Q z) --> (P x --> Q x)"; |
285 Goal "\\<exists>x. \\<forall>y z. (P y --> Q z) --> (P x --> Q x)"; |
286 by (meson_tac 1); |
286 by (meson_tac 1); |
287 result(); |
287 result(); |
288 |
288 |
289 writeln"Problem 20"; |
289 writeln"Problem 20"; |
290 Goal "(! x y. ? z. ! w. (P x & Q y --> R z & S w)) \ |
290 Goal "(\\<forall>x y. \\<exists>z. \\<forall>w. (P x & Q y --> R z & S w)) \ |
291 \ --> (? x y. P x & Q y) --> (? z. R z)"; |
291 \ --> (\\<exists>x y. P x & Q y) --> (\\<exists>z. R z)"; |
292 by (meson_tac 1); |
292 by (meson_tac 1); |
293 result(); |
293 result(); |
294 |
294 |
295 writeln"Problem 21"; |
295 writeln"Problem 21"; |
296 Goal "(? x. P --> Q x) & (? x. Q x --> P) --> (? x. P=Q x)"; |
296 Goal "(\\<exists>x. P --> Q x) & (\\<exists>x. Q x --> P) --> (\\<exists>x. P=Q x)"; |
297 by (meson_tac 1); |
297 by (meson_tac 1); |
298 result(); |
298 result(); |
299 |
299 |
300 writeln"Problem 22"; |
300 writeln"Problem 22"; |
301 Goal "(! x. P = Q x) --> (P = (! x. Q x))"; |
301 Goal "(\\<forall>x. P = Q x) --> (P = (\\<forall>x. Q x))"; |
302 by (meson_tac 1); |
302 by (meson_tac 1); |
303 result(); |
303 result(); |
304 |
304 |
305 writeln"Problem 23"; |
305 writeln"Problem 23"; |
306 Goal "(! x. P | Q x) = (P | (! x. Q x))"; |
306 Goal "(\\<forall>x. P | Q x) = (P | (\\<forall>x. Q x))"; |
307 by (meson_tac 1); |
307 by (meson_tac 1); |
308 result(); |
308 result(); |
309 |
309 |
310 writeln"Problem 24"; (*The first goal clause is useless*) |
310 writeln"Problem 24"; (*The first goal clause is useless*) |
311 Goal "~(? x. S x & Q x) & (! x. P x --> Q x | R x) & \ |
311 Goal "~(\\<exists>x. S x & Q x) & (\\<forall>x. P x --> Q x | R x) & \ |
312 \ (~(? x. P x) --> (? x. Q x)) & (! x. Q x | R x --> S x) \ |
312 \ (~(\\<exists>x. P x) --> (\\<exists>x. Q x)) & (\\<forall>x. Q x | R x --> S x) \ |
313 \ --> (? x. P x & R x)"; |
313 \ --> (\\<exists>x. P x & R x)"; |
314 by (meson_tac 1); |
314 by (meson_tac 1); |
315 result(); |
315 result(); |
316 |
316 |
317 writeln"Problem 25"; |
317 writeln"Problem 25"; |
318 Goal "(? x. P x) & \ |
318 Goal "(\\<exists>x. P x) & \ |
319 \ (! x. L x --> ~ (M x & R x)) & \ |
319 \ (\\<forall>x. L x --> ~ (M x & R x)) & \ |
320 \ (! x. P x --> (M x & L x)) & \ |
320 \ (\\<forall>x. P x --> (M x & L x)) & \ |
321 \ ((! x. P x --> Q x) | (? x. P x & R x)) \ |
321 \ ((\\<forall>x. P x --> Q x) | (\\<exists>x. P x & R x)) \ |
322 \ --> (? x. Q x & P x)"; |
322 \ --> (\\<exists>x. Q x & P x)"; |
323 by (meson_tac 1); |
323 by (meson_tac 1); |
324 result(); |
324 result(); |
325 |
325 |
326 writeln"Problem 26"; (*24 Horn clauses*) |
326 writeln"Problem 26"; (*24 Horn clauses*) |
327 Goal "((? x. p x) = (? x. q x)) & \ |
327 Goal "((\\<exists>x. p x) = (\\<exists>x. q x)) & \ |
328 \ (! x. ! y. p x & q y --> (r x = s y)) \ |
328 \ (\\<forall>x. \\<forall>y. p x & q y --> (r x = s y)) \ |
329 \ --> ((! x. p x --> r x) = (! x. q x --> s x))"; |
329 \ --> ((\\<forall>x. p x --> r x) = (\\<forall>x. q x --> s x))"; |
330 by (meson_tac 1); |
330 by (meson_tac 1); |
331 result(); |
331 result(); |
332 |
332 |
333 writeln"Problem 27"; (*13 Horn clauses*) |
333 writeln"Problem 27"; (*13 Horn clauses*) |
334 Goal "(? x. P x & ~Q x) & \ |
334 Goal "(\\<exists>x. P x & ~Q x) & \ |
335 \ (! x. P x --> R x) & \ |
335 \ (\\<forall>x. P x --> R x) & \ |
336 \ (! x. M x & L x --> P x) & \ |
336 \ (\\<forall>x. M x & L x --> P x) & \ |
337 \ ((? x. R x & ~ Q x) --> (! x. L x --> ~ R x)) \ |
337 \ ((\\<exists>x. R x & ~ Q x) --> (\\<forall>x. L x --> ~ R x)) \ |
338 \ --> (! x. M x --> ~L x)"; |
338 \ --> (\\<forall>x. M x --> ~L x)"; |
339 by (meson_tac 1); |
339 by (meson_tac 1); |
340 result(); |
340 result(); |
341 |
341 |
342 writeln"Problem 28. AMENDED"; (*14 Horn clauses*) |
342 writeln"Problem 28. AMENDED"; (*14 Horn clauses*) |
343 Goal "(! x. P x --> (! x. Q x)) & \ |
343 Goal "(\\<forall>x. P x --> (\\<forall>x. Q x)) & \ |
344 \ ((! x. Q x | R x) --> (? x. Q x & S x)) & \ |
344 \ ((\\<forall>x. Q x | R x) --> (\\<exists>x. Q x & S x)) & \ |
345 \ ((? x. S x) --> (! x. L x --> M x)) \ |
345 \ ((\\<exists>x. S x) --> (\\<forall>x. L x --> M x)) \ |
346 \ --> (! x. P x & L x --> M x)"; |
346 \ --> (\\<forall>x. P x & L x --> M x)"; |
347 by (meson_tac 1); |
347 by (meson_tac 1); |
348 result(); |
348 result(); |
349 |
349 |
350 writeln"Problem 29. Essentially the same as Principia Mathematica *11.71"; |
350 writeln"Problem 29. Essentially the same as Principia Mathematica *11.71"; |
351 (*62 Horn clauses*) |
351 (*62 Horn clauses*) |
352 Goal "(? x. F x) & (? y. G y) \ |
352 Goal "(\\<exists>x. F x) & (\\<exists>y. G y) \ |
353 \ --> ( ((! x. F x --> H x) & (! y. G y --> J y)) = \ |
353 \ --> ( ((\\<forall>x. F x --> H x) & (\\<forall>y. G y --> J y)) = \ |
354 \ (! x y. F x & G y --> H x & J y))"; |
354 \ (\\<forall>x y. F x & G y --> H x & J y))"; |
355 by (meson_tac 1); (*0.7 secs*) |
355 by (meson_tac 1); (*0.7 secs*) |
356 result(); |
356 result(); |
357 |
357 |
358 writeln"Problem 30"; |
358 writeln"Problem 30"; |
359 Goal "(! x. P x | Q x --> ~ R x) & \ |
359 Goal "(\\<forall>x. P x | Q x --> ~ R x) & \ |
360 \ (! x. (Q x --> ~ S x) --> P x & R x) \ |
360 \ (\\<forall>x. (Q x --> ~ S x) --> P x & R x) \ |
361 \ --> (! x. S x)"; |
361 \ --> (\\<forall>x. S x)"; |
362 by (meson_tac 1); |
362 by (meson_tac 1); |
363 result(); |
363 result(); |
364 |
364 |
365 writeln"Problem 31"; (*10 Horn clauses; first negative clauses is useless*) |
365 writeln"Problem 31"; (*10 Horn clauses; first negative clauses is useless*) |
366 Goal "~(? x. P x & (Q x | R x)) & \ |
366 Goal "~(\\<exists>x. P x & (Q x | R x)) & \ |
367 \ (? x. L x & P x) & \ |
367 \ (\\<exists>x. L x & P x) & \ |
368 \ (! x. ~ R x --> M x) \ |
368 \ (\\<forall>x. ~ R x --> M x) \ |
369 \ --> (? x. L x & M x)"; |
369 \ --> (\\<exists>x. L x & M x)"; |
370 by (meson_tac 1); |
370 by (meson_tac 1); |
371 result(); |
371 result(); |
372 |
372 |
373 writeln"Problem 32"; |
373 writeln"Problem 32"; |
374 Goal "(! x. P x & (Q x | R x)-->S x) & \ |
374 Goal "(\\<forall>x. P x & (Q x | R x)-->S x) & \ |
375 \ (! x. S x & R x --> L x) & \ |
375 \ (\\<forall>x. S x & R x --> L x) & \ |
376 \ (! x. M x --> R x) \ |
376 \ (\\<forall>x. M x --> R x) \ |
377 \ --> (! x. P x & M x --> L x)"; |
377 \ --> (\\<forall>x. P x & M x --> L x)"; |
378 by (meson_tac 1); |
378 by (meson_tac 1); |
379 result(); |
379 result(); |
380 |
380 |
381 writeln"Problem 33"; (*55 Horn clauses*) |
381 writeln"Problem 33"; (*55 Horn clauses*) |
382 Goal "(! x. P a & (P x --> P b)-->P c) = \ |
382 Goal "(\\<forall>x. P a & (P x --> P b)-->P c) = \ |
383 \ (! x. (~P a | P x | P c) & (~P a | ~P b | P c))"; |
383 \ (\\<forall>x. (~P a | P x | P c) & (~P a | ~P b | P c))"; |
384 by (meson_tac 1); (*5.6 secs*) |
384 by (meson_tac 1); (*5.6 secs*) |
385 result(); |
385 result(); |
386 |
386 |
387 writeln"Problem 34 AMENDED (TWICE!!)"; (*924 Horn clauses*) |
387 writeln"Problem 34 AMENDED (TWICE!!)"; (*924 Horn clauses*) |
388 (*Andrews's challenge*) |
388 (*Andrews's challenge*) |
389 Goal "((? x. ! y. p x = p y) = \ |
389 Goal "((\\<exists>x. \\<forall>y. p x = p y) = \ |
390 \ ((? x. q x) = (! y. p y))) = \ |
390 \ ((\\<exists>x. q x) = (\\<forall>y. p y))) = \ |
391 \ ((? x. ! y. q x = q y) = \ |
391 \ ((\\<exists>x. \\<forall>y. q x = q y) = \ |
392 \ ((? x. p x) = (! y. q y)))"; |
392 \ ((\\<exists>x. p x) = (\\<forall>y. q y)))"; |
393 by (meson_tac 1); (*13 secs*) |
393 by (meson_tac 1); (*13 secs*) |
394 result(); |
394 result(); |
395 |
395 |
396 writeln"Problem 35"; |
396 writeln"Problem 35"; |
397 Goal "? x y. P x y --> (! u v. P u v)"; |
397 Goal "\\<exists>x y. P x y --> (\\<forall>u v. P u v)"; |
398 by (meson_tac 1); |
398 by (meson_tac 1); |
399 result(); |
399 result(); |
400 |
400 |
401 writeln"Problem 36"; (*15 Horn clauses*) |
401 writeln"Problem 36"; (*15 Horn clauses*) |
402 Goal "(! x. ? y. J x y) & \ |
402 Goal "(\\<forall>x. \\<exists>y. J x y) & \ |
403 \ (! x. ? y. G x y) & \ |
403 \ (\\<forall>x. \\<exists>y. G x y) & \ |
404 \ (! x y. J x y | G x y --> \ |
404 \ (\\<forall>x y. J x y | G x y --> \ |
405 \ (! z. J y z | G y z --> H x z)) \ |
405 \ (\\<forall>z. J y z | G y z --> H x z)) \ |
406 \ --> (! x. ? y. H x y)"; |
406 \ --> (\\<forall>x. \\<exists>y. H x y)"; |
407 by (meson_tac 1); |
407 by (meson_tac 1); |
408 result(); |
408 result(); |
409 |
409 |
410 writeln"Problem 37"; (*10 Horn clauses*) |
410 writeln"Problem 37"; (*10 Horn clauses*) |
411 Goal "(! z. ? w. ! x. ? y. \ |
411 Goal "(\\<forall>z. \\<exists>w. \\<forall>x. \\<exists>y. \ |
412 \ (P x z --> P y w) & P y z & (P y w --> (? u. Q u w))) & \ |
412 \ (P x z --> P y w) & P y z & (P y w --> (\\<exists>u. Q u w))) & \ |
413 \ (! x z. ~P x z --> (? y. Q y z)) & \ |
413 \ (\\<forall>x z. ~P x z --> (\\<exists>y. Q y z)) & \ |
414 \ ((? x y. Q x y) --> (! x. R x x)) \ |
414 \ ((\\<exists>x y. Q x y) --> (\\<forall>x. R x x)) \ |
415 \ --> (! x. ? y. R x y)"; |
415 \ --> (\\<forall>x. \\<exists>y. R x y)"; |
416 by (meson_tac 1); (*causes unification tracing messages*) |
416 by (meson_tac 1); (*causes unification tracing messages*) |
417 result(); |
417 result(); |
418 |
418 |
419 writeln"Problem 38"; (*Quite hard: 422 Horn clauses!!*) |
419 writeln"Problem 38"; (*Quite hard: 422 Horn clauses!!*) |
420 Goal "(! x. p a & (p x --> (? y. p y & r x y)) --> \ |
420 Goal "(\\<forall>x. p a & (p x --> (\\<exists>y. p y & r x y)) --> \ |
421 \ (? z. ? w. p z & r x w & r w z)) = \ |
421 \ (\\<exists>z. \\<exists>w. p z & r x w & r w z)) = \ |
422 \ (! x. (~p a | p x | (? z. ? w. p z & r x w & r w z)) & \ |
422 \ (\\<forall>x. (~p a | p x | (\\<exists>z. \\<exists>w. p z & r x w & r w z)) & \ |
423 \ (~p a | ~(? y. p y & r x y) | \ |
423 \ (~p a | ~(\\<exists>y. p y & r x y) | \ |
424 \ (? z. ? w. p z & r x w & r w z)))"; |
424 \ (\\<exists>z. \\<exists>w. p z & r x w & r w z)))"; |
425 by (safe_best_meson_tac 1); (*10 secs; iter. deepening is slightly slower*) |
425 by (safe_best_meson_tac 1); (*10 secs; iter. deepening is slightly slower*) |
426 result(); |
426 result(); |
427 |
427 |
428 writeln"Problem 39"; |
428 writeln"Problem 39"; |
429 Goal "~ (? x. ! y. F y x = (~F y y))"; |
429 Goal "~ (\\<exists>x. \\<forall>y. F y x = (~F y y))"; |
430 by (meson_tac 1); |
430 by (meson_tac 1); |
431 result(); |
431 result(); |
432 |
432 |
433 writeln"Problem 40. AMENDED"; |
433 writeln"Problem 40. AMENDED"; |
434 Goal "(? y. ! x. F x y = F x x) \ |
434 Goal "(\\<exists>y. \\<forall>x. F x y = F x x) \ |
435 \ --> ~ (! x. ? y. ! z. F z y = (~F z x))"; |
435 \ --> ~ (\\<forall>x. \\<exists>y. \\<forall>z. F z y = (~F z x))"; |
436 by (meson_tac 1); |
436 by (meson_tac 1); |
437 result(); |
437 result(); |
438 |
438 |
439 writeln"Problem 41"; |
439 writeln"Problem 41"; |
440 Goal "(! z. (? y. (! x. f x y = (f x z & ~ f x x)))) \ |
440 Goal "(\\<forall>z. (\\<exists>y. (\\<forall>x. f x y = (f x z & ~ f x x)))) \ |
441 \ --> ~ (? z. ! x. f x z)"; |
441 \ --> ~ (\\<exists>z. \\<forall>x. f x z)"; |
442 by (meson_tac 1); |
442 by (meson_tac 1); |
443 result(); |
443 result(); |
444 |
444 |
445 writeln"Problem 42"; |
445 writeln"Problem 42"; |
446 Goal "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))"; |
446 Goal "~ (\\<exists>y. \\<forall>x. p x y = (~ (\\<exists>z. p x z & p z x)))"; |
447 by (meson_tac 1); |
447 by (meson_tac 1); |
448 result(); |
448 result(); |
449 |
449 |
450 writeln"Problem 43 NOW PROVED AUTOMATICALLY!!"; |
450 writeln"Problem 43 NOW PROVED AUTOMATICALLY!!"; |
451 Goal "(! x. ! y. q x y = (! z. p z x = (p z y::bool))) \ |
451 Goal "(\\<forall>x. \\<forall>y. q x y = (\\<forall>z. p z x = (p z y::bool))) \ |
452 \ --> (! x. (! y. q x y = (q y x::bool)))"; |
452 \ --> (\\<forall>x. (\\<forall>y. q x y = (q y x::bool)))"; |
453 by (safe_best_meson_tac 1); |
453 by (safe_best_meson_tac 1); |
454 (*1.6 secs; iter. deepening is slightly slower*) |
454 (*1.6 secs; iter. deepening is slightly slower*) |
455 result(); |
455 result(); |
456 |
456 |
457 writeln"Problem 44"; (*13 Horn clauses; 7-step proof*) |
457 writeln"Problem 44"; (*13 Horn clauses; 7-step proof*) |
458 Goal "(! x. f x --> \ |
458 Goal "(\\<forall>x. f x --> \ |
459 \ (? y. g y & h x y & (? y. g y & ~ h x y))) & \ |
459 \ (\\<exists>y. g y & h x y & (\\<exists>y. g y & ~ h x y))) & \ |
460 \ (? x. j x & (! y. g y --> h x y)) \ |
460 \ (\\<exists>x. j x & (\\<forall>y. g y --> h x y)) \ |
461 \ --> (? x. j x & ~f x)"; |
461 \ --> (\\<exists>x. j x & ~f x)"; |
462 by (meson_tac 1); |
462 by (meson_tac 1); |
463 result(); |
463 result(); |
464 |
464 |
465 writeln"Problem 45"; (*27 Horn clauses; 54-step proof*) |
465 writeln"Problem 45"; (*27 Horn clauses; 54-step proof*) |
466 Goal "(! x. f x & (! y. g y & h x y --> j x y) \ |
466 Goal "(\\<forall>x. f x & (\\<forall>y. g y & h x y --> j x y) \ |
467 \ --> (! y. g y & h x y --> k y)) & \ |
467 \ --> (\\<forall>y. g y & h x y --> k y)) & \ |
468 \ ~ (? y. l y & k y) & \ |
468 \ ~ (\\<exists>y. l y & k y) & \ |
469 \ (? x. f x & (! y. h x y --> l y) \ |
469 \ (\\<exists>x. f x & (\\<forall>y. h x y --> l y) \ |
470 \ & (! y. g y & h x y --> j x y)) \ |
470 \ & (\\<forall>y. g y & h x y --> j x y)) \ |
471 \ --> (? x. f x & ~ (? y. g y & h x y))"; |
471 \ --> (\\<exists>x. f x & ~ (\\<exists>y. g y & h x y))"; |
472 by (safe_best_meson_tac 1); |
472 by (safe_best_meson_tac 1); |
473 (*1.6 secs; iter. deepening is slightly slower*) |
473 (*1.6 secs; iter. deepening is slightly slower*) |
474 result(); |
474 result(); |
475 |
475 |
476 writeln"Problem 46"; (*26 Horn clauses; 21-step proof*) |
476 writeln"Problem 46"; (*26 Horn clauses; 21-step proof*) |
477 Goal "(! x. f x & (! y. f y & h y x --> g y) --> g x) & \ |
477 Goal "(\\<forall>x. f x & (\\<forall>y. f y & h y x --> g y) --> g x) & \ |
478 \ ((? x. f x & ~g x) --> \ |
478 \ ((\\<exists>x. f x & ~g x) --> \ |
479 \ (? x. f x & ~g x & (! y. f y & ~g y --> j x y))) & \ |
479 \ (\\<exists>x. f x & ~g x & (\\<forall>y. f y & ~g y --> j x y))) & \ |
480 \ (! x y. f x & f y & h x y --> ~j y x) \ |
480 \ (\\<forall>x y. f x & f y & h x y --> ~j y x) \ |
481 \ --> (! x. f x --> g x)"; |
481 \ --> (\\<forall>x. f x --> g x)"; |
482 by (safe_best_meson_tac 1); |
482 by (safe_best_meson_tac 1); |
483 (*1.7 secs; iter. deepening is slightly slower*) |
483 (*1.7 secs; iter. deepening is slightly slower*) |
484 result(); |
484 result(); |
485 |
485 |
486 writeln"Problem 47. Schubert's Steamroller"; |
486 writeln"Problem 47. Schubert's Steamroller"; |
487 (*26 clauses; 63 Horn clauses |
487 (*26 clauses; 63 Horn clauses |
488 87094 inferences so far. Searching to depth 36*) |
488 87094 inferences so far. Searching to depth 36*) |
489 Goal "(! x. P1 x --> P0 x) & (? x. P1 x) & \ |
489 Goal "(\\<forall>x. P1 x --> P0 x) & (\\<exists>x. P1 x) & \ |
490 \ (! x. P2 x --> P0 x) & (? x. P2 x) & \ |
490 \ (\\<forall>x. P2 x --> P0 x) & (\\<exists>x. P2 x) & \ |
491 \ (! x. P3 x --> P0 x) & (? x. P3 x) & \ |
491 \ (\\<forall>x. P3 x --> P0 x) & (\\<exists>x. P3 x) & \ |
492 \ (! x. P4 x --> P0 x) & (? x. P4 x) & \ |
492 \ (\\<forall>x. P4 x --> P0 x) & (\\<exists>x. P4 x) & \ |
493 \ (! x. P5 x --> P0 x) & (? x. P5 x) & \ |
493 \ (\\<forall>x. P5 x --> P0 x) & (\\<exists>x. P5 x) & \ |
494 \ (! x. Q1 x --> Q0 x) & (? x. Q1 x) & \ |
494 \ (\\<forall>x. Q1 x --> Q0 x) & (\\<exists>x. Q1 x) & \ |
495 \ (! x. P0 x --> ((! y. Q0 y-->R x y) | \ |
495 \ (\\<forall>x. P0 x --> ((\\<forall>y. Q0 y-->R x y) | \ |
496 \ (! y. P0 y & S y x & \ |
496 \ (\\<forall>y. P0 y & S y x & \ |
497 \ (? z. Q0 z&R y z) --> R x y))) & \ |
497 \ (\\<exists>z. Q0 z&R y z) --> R x y))) & \ |
498 \ (! x y. P3 y & (P5 x|P4 x) --> S x y) & \ |
498 \ (\\<forall>x y. P3 y & (P5 x|P4 x) --> S x y) & \ |
499 \ (! x y. P3 x & P2 y --> S x y) & \ |
499 \ (\\<forall>x y. P3 x & P2 y --> S x y) & \ |
500 \ (! x y. P2 x & P1 y --> S x y) & \ |
500 \ (\\<forall>x y. P2 x & P1 y --> S x y) & \ |
501 \ (! x y. P1 x & (P2 y|Q1 y) --> ~R x y) & \ |
501 \ (\\<forall>x y. P1 x & (P2 y|Q1 y) --> ~R x y) & \ |
502 \ (! x y. P3 x & P4 y --> R x y) & \ |
502 \ (\\<forall>x y. P3 x & P4 y --> R x y) & \ |
503 \ (! x y. P3 x & P5 y --> ~R x y) & \ |
503 \ (\\<forall>x y. P3 x & P5 y --> ~R x y) & \ |
504 \ (! x. (P4 x|P5 x) --> (? y. Q0 y & R x y)) \ |
504 \ (\\<forall>x. (P4 x|P5 x) --> (\\<exists>y. Q0 y & R x y)) \ |
505 \ --> (? x y. P0 x & P0 y & (? z. Q1 z & R y z & R x y))"; |
505 \ --> (\\<exists>x y. P0 x & P0 y & (\\<exists>z. Q1 z & R y z & R x y))"; |
506 by (safe_best_meson_tac 1); (*MUCH faster than iterative deepening*) |
506 by (safe_best_meson_tac 1); (*MUCH faster than iterative deepening*) |
507 result(); |
507 result(); |
508 |
508 |
509 (*The Los problem? Circulated by John Harrison*) |
509 (*The Los problem\\<exists> Circulated by John Harrison*) |
510 Goal "(! x y z. P x y & P y z --> P x z) & \ |
510 Goal "(\\<forall>x y z. P x y & P y z --> P x z) & \ |
511 \ (! x y z. Q x y & Q y z --> Q x z) & \ |
511 \ (\\<forall>x y z. Q x y & Q y z --> Q x z) & \ |
512 \ (! x y. P x y --> P y x) & \ |
512 \ (\\<forall>x y. P x y --> P y x) & \ |
513 \ (! x y. P x y | Q x y) \ |
513 \ (\\<forall>x y. P x y | Q x y) \ |
514 \ --> (! x y. P x y) | (! x y. Q x y)"; |
514 \ --> (\\<forall>x y. P x y) | (\\<forall>x y. Q x y)"; |
515 by (safe_best_meson_tac 1); (*2.3 secs; iter. deepening is VERY slow*) |
515 by (safe_best_meson_tac 1); (*2.3 secs; iter. deepening is VERY slow*) |
516 result(); |
516 result(); |
517 |
517 |
518 (*A similar example, suggested by Johannes Schumann and credited to Pelletier*) |
518 (*A similar example, suggested by Johannes Schumann and credited to Pelletier*) |
519 Goal "(!x y z. P x y --> P y z --> P x z) --> \ |
519 Goal "(!x y z. P x y --> P y z --> P x z) --> \ |