1586

1 
(* Title: HOL/ex/mesontest

969

2 
ID: $Id$

1465

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

969

4 
Copyright 1992 University of Cambridge


5 


6 
Test data for the MESON proof procedure


7 
(Excludes the equality problems 51, 52, 56, 58)


8 


9 
show_hyps:=false;


10 

1586

11 
full_deriv:=false;

969

12 
by (rtac ccontr 1);


13 
val [prem] = gethyps 1;


14 
val nnf = make_nnf prem;


15 
val xsko = skolemize nnf;


16 
by (cut_facts_tac [xsko] 1 THEN REPEAT (etac exE 1));


17 
val [_,sko] = gethyps 1;

1465

18 
val clauses = make_clauses [sko];

969

19 
val horns = make_horns clauses;

1586

20 
val goes = neg_clauses clauses;

969

21 


22 
goal HOL.thy "False";

1586

23 
by (resolve_tac (map make_goal goes) 1);


24 
full_deriv:=true;


25 

969

26 
by (prolog_step_tac horns 1);


27 
by (depth_prolog_tac horns);


28 
by (best_prolog_tac size_of_subgoals horns);


29 
*)


30 


31 
writeln"File HOL/ex/mesontest.";


32 

1586

33 
(*Deep unifications can be required, esp. during transformation to clauses*)


34 
val orig_trace_bound = !Unify.trace_bound


35 
and orig_search_bound = !Unify.search_bound;


36 
Unify.trace_bound := 20;


37 
Unify.search_bound := 40;


38 

969

39 
(**** Interactive examples ****)


40 


41 
(*Generate nice names for Skolem functions*)


42 
Logic.auto_rename := true; Logic.set_rename_prefix "a";


43 


44 


45 
writeln"Problem 25";

1586

46 
goal HOL.thy "(? x. P x) & \


47 
\ (! x. L x > ~ (M x & R x)) & \


48 
\ (! x. P x > (M x & L x)) & \


49 
\ ((! x. P x > Q x)  (? x. P x & R x)) \


50 
\ > (? x. Q x & P x)";

969

51 
by (rtac ccontr 1);


52 
val [prem25] = gethyps 1;


53 
val nnf25 = make_nnf prem25;


54 
val xsko25 = skolemize nnf25;


55 
by (cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1));


56 
val [_,sko25] = gethyps 1;

1465

57 
val clauses25 = make_clauses [sko25]; (*7 clauses*)


58 
val horns25 = make_horns clauses25; (*16 Horn clauses*)

969

59 
val go25::_ = neg_clauses clauses25;


60 


61 
goal HOL.thy "False";


62 
by (rtac (make_goal go25) 1);


63 
by (depth_prolog_tac horns25);


64 


65 


66 
writeln"Problem 26";

1586

67 
goal HOL.thy "((? x. p x) = (? x. q x)) & \


68 
\ (! x. ! y. p x & q y > (r x = s y)) \


69 
\ > ((! x. p x > r x) = (! x. q x > s x))";

969

70 
by (rtac ccontr 1);


71 
val [prem26] = gethyps 1;


72 
val nnf26 = make_nnf prem26;


73 
val xsko26 = skolemize nnf26;


74 
by (cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1));


75 
val [_,sko26] = gethyps 1;

1465

76 
val clauses26 = make_clauses [sko26]; (*9 clauses*)


77 
val horns26 = make_horns clauses26; (*24 Horn clauses*)

969

78 
val go26::_ = neg_clauses clauses26;


79 


80 
goal HOL.thy "False";


81 
by (rtac (make_goal go26) 1);

1586

82 
by (depth_prolog_tac horns26); (*1.4 secs*)


83 
(*Proof is of length 107!!*)

969

84 


85 

1586

86 
writeln"Problem 43 NOW PROVED AUTOMATICALLY!!"; (*16 Horn clauses*)

1465

87 
goal HOL.thy "(! x. ! y. q x y = (! z. p z x = (p z y::bool))) \

969

88 
\ > (! x. (! y. q x y = (q y x::bool)))";


89 
by (rtac ccontr 1);


90 
val [prem43] = gethyps 1;


91 
val nnf43 = make_nnf prem43;


92 
val xsko43 = skolemize nnf43;


93 
by (cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1));


94 
val [_,sko43] = gethyps 1;

1465

95 
val clauses43 = make_clauses [sko43]; (*6*)


96 
val horns43 = make_horns clauses43; (*16*)

969

97 
val go43::_ = neg_clauses clauses43;


98 


99 
goal HOL.thy "False";


100 
by (rtac (make_goal go43) 1);

1586

101 
by (best_prolog_tac size_of_subgoals horns43); (*1.6 secs*)


102 


103 
(*


104 
#1 (q x xa ==> ~ q x xa) ==> q xa x


105 
#2 (q xa x ==> ~ q xa x) ==> q x xa


106 
#3 (~ q x xa ==> q x xa) ==> ~ q xa x


107 
#4 (~ q xa x ==> q xa x) ==> ~ q x xa


108 
#5 [ ~ q ?U ?V ==> q ?U ?V; ~ p ?W ?U ==> p ?W ?U ] ==> p ?W ?V


109 
#6 [ ~ p ?W ?U ==> p ?W ?U; p ?W ?V ==> ~ p ?W ?V ] ==> ~ q ?U ?V


110 
#7 [ p ?W ?V ==> ~ p ?W ?V; ~ q ?U ?V ==> q ?U ?V ] ==> ~ p ?W ?U


111 
#8 [ ~ q ?U ?V ==> q ?U ?V; ~ p ?W ?V ==> p ?W ?V ] ==> p ?W ?U


112 
#9 [ ~ p ?W ?V ==> p ?W ?V; p ?W ?U ==> ~ p ?W ?U ] ==> ~ q ?U ?V


113 
#10 [ p ?W ?U ==> ~ p ?W ?U; ~ q ?U ?V ==> q ?U ?V ] ==> ~ p ?W ?V


114 
#11 [ p (xb ?U ?V) ?U ==> ~ p (xb ?U ?V) ?U;


115 
p (xb ?U ?V) ?V ==> ~ p (xb ?U ?V) ?V ] ==> q ?U ?V


116 
#12 [ p (xb ?U ?V) ?V ==> ~ p (xb ?U ?V) ?V; q ?U ?V ==> ~ q ?U ?V ] ==>


117 
p (xb ?U ?V) ?U


118 
#13 [ q ?U ?V ==> ~ q ?U ?V; p (xb ?U ?V) ?U ==> ~ p (xb ?U ?V) ?U ] ==>


119 
p (xb ?U ?V) ?V


120 
#14 [ ~ p (xb ?U ?V) ?U ==> p (xb ?U ?V) ?U;


121 
~ p (xb ?U ?V) ?V ==> p (xb ?U ?V) ?V ] ==> q ?U ?V


122 
#15 [ ~ p (xb ?U ?V) ?V ==> p (xb ?U ?V) ?V; q ?U ?V ==> ~ q ?U ?V ] ==>


123 
~ p (xb ?U ?V) ?U


124 
#16 [ q ?U ?V ==> ~ q ?U ?V; ~ p (xb ?U ?V) ?U ==> p (xb ?U ?V) ?U ] ==>


125 
~ p (xb ?U ?V) ?V


126 


127 
And here is the proof! (Unkn is the start state after use of goal clause)


128 
[Unkn, Res ([Thm "#14"], false, 1), Res ([Thm "#5"], false, 1),


129 
Res ([Thm "#1"], false, 1), Asm 1, Res ([Thm "#13"], false, 1), Asm 2,


130 
Asm 1, Res ([Thm "#13"], false, 1), Asm 1, Res ([Thm "#10"], false, 1),


131 
Res ([Thm "#16"], false, 1), Asm 2, Asm 1, Res ([Thm "#1"], false, 1),


132 
Asm 1, Res ([Thm "#14"], false, 1), Res ([Thm "#5"], false, 1),


133 
Res ([Thm "#2"], false, 1), Asm 1, Res ([Thm "#13"], false, 1), Asm 2,


134 
Asm 1, Res ([Thm "#8"], false, 1), Res ([Thm "#2"], false, 1), Asm 1,


135 
Res ([Thm "#12"], false, 1), Asm 2, Asm 1] : lderiv list


136 
*)

969

137 


138 


139 
(*Restore variable name preservation*)


140 
Logic.auto_rename := false;


141 


142 


143 
(**** Batch test data ****)


144 


145 
(*Sample problems from


146 
F. J. Pelletier,


147 
SeventyFive Problems for Testing Automatic Theorem Provers,


148 
J. Automated Reasoning 2 (1986), 191216.


149 
Errata, JAR 4 (1988), 236236.


150 


151 
The hardest problems  judging by experience with several theorem provers,


152 
including matrix ones  are 34 and 43.


153 
*)


154 


155 
writeln"Pelletier's examples";


156 
(*1*)

1586

157 
goal HOL.thy "(P > Q) = (~Q > ~P)";

969

158 
by (safe_meson_tac 1);


159 
result();


160 


161 
(*2*)


162 
goal HOL.thy "(~ ~ P) = P";


163 
by (safe_meson_tac 1);


164 
result();


165 


166 
(*3*)


167 
goal HOL.thy "~(P>Q) > (Q>P)";


168 
by (safe_meson_tac 1);


169 
result();


170 


171 
(*4*)


172 
goal HOL.thy "(~P>Q) = (~Q > P)";


173 
by (safe_meson_tac 1);


174 
result();


175 


176 
(*5*)


177 
goal HOL.thy "((PQ)>(PR)) > (P(Q>R))";


178 
by (safe_meson_tac 1);


179 
result();


180 


181 
(*6*)


182 
goal HOL.thy "P  ~ P";


183 
by (safe_meson_tac 1);


184 
result();


185 


186 
(*7*)


187 
goal HOL.thy "P  ~ ~ ~ P";


188 
by (safe_meson_tac 1);


189 
result();


190 


191 
(*8. Peirce's law*)


192 
goal HOL.thy "((P>Q) > P) > P";


193 
by (safe_meson_tac 1);


194 
result();


195 


196 
(*9*)


197 
goal HOL.thy "((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)";


198 
by (safe_meson_tac 1);


199 
result();


200 


201 
(*10*)


202 
goal HOL.thy "(Q>R) & (R>P&Q) & (P>QR) > (P=Q)";


203 
by (safe_meson_tac 1);


204 
result();


205 


206 
(*11. Proved in each direction (incorrectly, says Pelletier!!) *)


207 
goal HOL.thy "P=(P::bool)";


208 
by (safe_meson_tac 1);


209 
result();


210 


211 
(*12. "Dijkstra's law"*)


212 
goal HOL.thy "((P = Q) = R) = (P = (Q = R))";

1586

213 
by (safe_meson_tac 1);

969

214 
result();


215 


216 
(*13. Distributive law*)


217 
goal HOL.thy "(P  (Q & R)) = ((P  Q) & (P  R))";


218 
by (safe_meson_tac 1);


219 
result();


220 


221 
(*14*)


222 
goal HOL.thy "(P = Q) = ((Q  ~P) & (~QP))";


223 
by (safe_meson_tac 1);


224 
result();


225 


226 
(*15*)


227 
goal HOL.thy "(P > Q) = (~P  Q)";


228 
by (safe_meson_tac 1);


229 
result();


230 


231 
(*16*)


232 
goal HOL.thy "(P>Q)  (Q>P)";


233 
by (safe_meson_tac 1);


234 
result();


235 


236 
(*17*)


237 
goal HOL.thy "((P & (Q>R))>S) = ((~P  Q  S) & (~P  ~R  S))";


238 
by (safe_meson_tac 1);


239 
result();


240 


241 
writeln"Classical Logic: examples with quantifiers";


242 

1586

243 
goal HOL.thy "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))";

969

244 
by (safe_meson_tac 1);


245 
result();


246 

1586

247 
goal HOL.thy "(? x. P > Q x) = (P > (? x.Q x))";

969

248 
by (safe_meson_tac 1);


249 
result();


250 

1586

251 
goal HOL.thy "(? x.P x > Q) = ((! x.P x) > Q)";

969

252 
by (safe_meson_tac 1);


253 
result();


254 

1586

255 
goal HOL.thy "((! x.P x)  Q) = (! x. P x  Q)";

969

256 
by (safe_meson_tac 1);


257 
result();


258 

1586

259 
goal HOL.thy "(! x. P x > P(f x)) & P d > P(f(f(f d)))";

969

260 
by (safe_meson_tac 1);


261 
result();


262 

1259

263 
(*Needs double instantiation of EXISTS*)

1586

264 
goal HOL.thy "? x. P x > P a & P b";

969

265 
by (safe_meson_tac 1);


266 
result();


267 

1586

268 
goal HOL.thy "? z. P z > (! x. P x)";

969

269 
by (safe_meson_tac 1);


270 
result();


271 


272 
writeln"Hard examples with quantifiers";


273 


274 
writeln"Problem 18";

1586

275 
goal HOL.thy "? y. ! x. P y > P x";

969

276 
by (safe_meson_tac 1);


277 
result();


278 


279 
writeln"Problem 19";

1586

280 
goal HOL.thy "? x. ! y z. (P y > Q z) > (P x > Q x)";

969

281 
by (safe_meson_tac 1);


282 
result();


283 


284 
writeln"Problem 20";

1586

285 
goal HOL.thy "(! x y. ? z. ! w. (P x & Q y > R z & S w)) \


286 
\ > (? x y. P x & Q y) > (? z. R z)";

969

287 
by (safe_meson_tac 1);


288 
result();


289 


290 
writeln"Problem 21";

1586

291 
goal HOL.thy "(? x. P > Q x) & (? x. Q x > P) > (? x. P=Q x)";

969

292 
by (safe_meson_tac 1);


293 
result();


294 


295 
writeln"Problem 22";

1586

296 
goal HOL.thy "(! x. P = Q x) > (P = (! x. Q x))";

969

297 
by (safe_meson_tac 1);


298 
result();


299 


300 
writeln"Problem 23";

1586

301 
goal HOL.thy "(! x. P  Q x) = (P  (! x. Q x))";

969

302 
by (safe_meson_tac 1);


303 
result();


304 

1586

305 
writeln"Problem 24"; (*The first goal clause is useless*)


306 
goal HOL.thy "~(? x. S x & Q x) & (! x. P x > Q x  R x) & \


307 
\ ~(? x.P x) > (? x.Q x) & (! x. Q x  R x > S x) \


308 
\ > (? x. P x & R x)";

969

309 
by (safe_meson_tac 1);


310 
result();


311 


312 
writeln"Problem 25";

1586

313 
goal HOL.thy "(? x. P x) & \


314 
\ (! x. L x > ~ (M x & R x)) & \


315 
\ (! x. P x > (M x & L x)) & \


316 
\ ((! x. P x > Q x)  (? x. P x & R x)) \


317 
\ > (? x. Q x & P x)";

969

318 
by (safe_meson_tac 1);


319 
result();


320 

1586

321 
writeln"Problem 26"; (*24 Horn clauses*)


322 
goal HOL.thy "((? x. p x) = (? x. q x)) & \


323 
\ (! x. ! y. p x & q y > (r x = s y)) \


324 
\ > ((! x. p x > r x) = (! x. q x > s x))";

969

325 
by (safe_meson_tac 1);


326 
result();


327 

1586

328 
writeln"Problem 27"; (*13 Horn clauses*)


329 
goal HOL.thy "(? x. P x & ~Q x) & \


330 
\ (! x. P x > R x) & \


331 
\ (! x. M x & L x > P x) & \


332 
\ ((? x. R x & ~ Q x) > (! x. L x > ~ R x)) \


333 
\ > (! x. M x > ~L x)";

969

334 
by (safe_meson_tac 1);


335 
result();


336 

1586

337 
writeln"Problem 28. AMENDED"; (*14 Horn clauses*)


338 
goal HOL.thy "(! x. P x > (! x. Q x)) & \


339 
\ ((! x. Q x  R x) > (? x. Q x & S x)) & \


340 
\ ((? x.S x) > (! x. L x > M x)) \


341 
\ > (! x. P x & L x > M x)";

969

342 
by (safe_meson_tac 1);


343 
result();


344 


345 
writeln"Problem 29. Essentially the same as Principia Mathematica *11.71";

1586

346 
(*62 Horn clauses*)


347 
goal HOL.thy "(? x. F x) & (? y. G y) \


348 
\ > ( ((! x. F x > H x) & (! y. G y > J y)) = \


349 
\ (! x y. F x & G y > H x & J y))";


350 
by (safe_meson_tac 1); (*0.7 secs*)

969

351 
result();


352 


353 
writeln"Problem 30";

1586

354 
goal HOL.thy "(! x. P x  Q x > ~ R x) & \


355 
\ (! x. (Q x > ~ S x) > P x & R x) \


356 
\ > (! x. S x)";

969

357 
by (safe_meson_tac 1);


358 
result();


359 

1586

360 
writeln"Problem 31"; (*10 Horn clauses; first negative clauses is useless*)


361 
goal HOL.thy "~(? x.P x & (Q x  R x)) & \


362 
\ (? x. L x & P x) & \


363 
\ (! x. ~ R x > M x) \


364 
\ > (? x. L x & M x)";

969

365 
by (safe_meson_tac 1);


366 
result();


367 


368 
writeln"Problem 32";

1586

369 
goal HOL.thy "(! x. P x & (Q x  R x)>S x) & \


370 
\ (! x. S x & R x > L x) & \


371 
\ (! x. M x > R x) \


372 
\ > (! x. P x & M x > L x)";

969

373 
by (safe_meson_tac 1);


374 
result();


375 

1586

376 
writeln"Problem 33"; (*55 Horn clauses*)


377 
goal HOL.thy "(! x. P a & (P x > P b)>P c) = \


378 
\ (! x. (~P a  P x  P c) & (~P a  ~P b  P c))";

1465

379 
by (safe_meson_tac 1); (*5.6 secs*)

969

380 
result();


381 

1586

382 
writeln"Problem 34 AMENDED (TWICE!!)"; (*924 Horn clauses*)

969

383 
(*Andrews's challenge*)

1586

384 
goal HOL.thy "((? x. ! y. p x = p y) = \


385 
\ ((? x. q x) = (! y. p y))) = \


386 
\ ((? x. ! y. q x = q y) = \


387 
\ ((? x. p x) = (! y. q y)))";


388 
by (safe_meson_tac 1); (*13 secs*)

969

389 
result();


390 


391 
writeln"Problem 35";


392 
goal HOL.thy "? x y. P x y > (! u v. P u v)";


393 
by (safe_meson_tac 1);


394 
result();


395 

1586

396 
writeln"Problem 36"; (*15 Horn clauses*)

969

397 
goal HOL.thy "(! x. ? y. J x y) & \


398 
\ (! x. ? y. G x y) & \

1465

399 
\ (! x y. J x y  G x y > \

969

400 
\ (! z. J y z  G y z > H x z)) \


401 
\ > (! x. ? y. H x y)";


402 
by (safe_meson_tac 1);


403 
result();


404 

1586

405 
writeln"Problem 37"; (*10 Horn clauses*)

969

406 
goal HOL.thy "(! z. ? w. ! x. ? y. \

1586

407 
\ (P x z > P y w) & P y z & (P y w > (? u.Q u w))) & \

969

408 
\ (! x z. ~P x z > (? y. Q y z)) & \


409 
\ ((? x y. Q x y) > (! x. R x x)) \


410 
\ > (! x. ? y. R x y)";


411 
by (safe_meson_tac 1); (*causes unification tracing messages*)


412 
result();


413 

1586

414 
writeln"Problem 38"; (*Quite hard: 422 Horn clauses!!*)

969

415 
goal HOL.thy

1586

416 
"(! x. p a & (p x > (? y. p y & r x y)) > \


417 
\ (? z. ? w. p z & r x w & r w z)) = \


418 
\ (! x. (~p a  p x  (? z. ? w. p z & r x w & r w z)) & \


419 
\ (~p a  ~(? y. p y & r x y)  \


420 
\ (? z. ? w. p z & r x w & r w z)))";


421 
by (safe_best_meson_tac 1); (*10 secs; iter. deepening is slightly slower*)

969

422 
result();


423 


424 
writeln"Problem 39";


425 
goal HOL.thy "~ (? x. ! y. F y x = (~F y y))";


426 
by (safe_meson_tac 1);


427 
result();


428 


429 
writeln"Problem 40. AMENDED";


430 
goal HOL.thy "(? y. ! x. F x y = F x x) \


431 
\ > ~ (! x. ? y. ! z. F z y = (~F z x))";


432 
by (safe_meson_tac 1);


433 
result();


434 


435 
writeln"Problem 41";

1465

436 
goal HOL.thy "(! z. (? y. (! x. f x y = (f x z & ~ f x x)))) \

969

437 
\ > ~ (? z. ! x. f x z)";


438 
by (safe_meson_tac 1);


439 
result();


440 


441 
writeln"Problem 42";


442 
goal HOL.thy "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))";


443 
by (safe_meson_tac 1);


444 
result();


445 


446 
writeln"Problem 43 NOW PROVED AUTOMATICALLY!!";

1465

447 
goal HOL.thy "(! x. ! y. q x y = (! z. p z x = (p z y::bool))) \

969

448 
\ > (! x. (! y. q x y = (q y x::bool)))";

1586

449 
by (safe_best_meson_tac 1);


450 
(*1.6 secs; iter. deepening is slightly slower*)

969

451 
result();


452 

1586

453 
writeln"Problem 44"; (*13 Horn clauses; 7step proof*)


454 
goal HOL.thy "(! x. f x > \


455 
\ (? y. g y & h x y & (? y. g y & ~ h x y))) & \


456 
\ (? x. j x & (! y. g y > h x y)) \


457 
\ > (? x. j x & ~f x)";

969

458 
by (safe_meson_tac 1);


459 
result();


460 

1586

461 
writeln"Problem 45"; (*27 Horn clauses; 54step proof*)


462 
goal HOL.thy "(! x. f x & (! y. g y & h x y > j x y) \


463 
\ > (! y. g y & h x y > k y)) & \


464 
\ ~ (? y. l y & k y) & \


465 
\ (? x. f x & (! y. h x y > l y) \


466 
\ & (! y. g y & h x y > j x y)) \


467 
\ > (? x. f x & ~ (? y. g y & h x y))";


468 
by (safe_best_meson_tac 1);


469 
(*1.6 secs; iter. deepening is slightly slower*)


470 
result();


471 


472 
writeln"Problem 46"; (*26 Horn clauses; 21step proof*)


473 
goal HOL.thy


474 
"(! x. f x & (! y. f y & h y x > g y) > g x) & \


475 
\ ((? x.f x & ~g x) > \


476 
\ (? x. f x & ~g x & (! y. f y & ~g y > j x y))) & \


477 
\ (! x y. f x & f y & h x y > ~j y x) \


478 
\ > (! x. f x > g x)";


479 
by (safe_best_meson_tac 1);


480 
(*1.7 secs; iter. deepening is slightly slower*)

969

481 
result();


482 

1586

483 
writeln"Problem 47. Schubert's Steamroller";


484 
(*26 clauses; 63 Horn clauses*)

969

485 
goal HOL.thy

1586

486 
"(! x. P1 x > P0 x) & (? x.P1 x) & \


487 
\ (! x. P2 x > P0 x) & (? x.P2 x) & \


488 
\ (! x. P3 x > P0 x) & (? x.P3 x) & \


489 
\ (! x. P4 x > P0 x) & (? x.P4 x) & \


490 
\ (! x. P5 x > P0 x) & (? x.P5 x) & \


491 
\ (! x. Q1 x > Q0 x) & (? x.Q1 x) & \


492 
\ (! x. P0 x > ((! y.Q0 y>R x y)  \


493 
\ (! y.P0 y & S y x & \


494 
\ (? z.Q0 z&R y z) > R x y))) & \


495 
\ (! x y. P3 y & (P5 xP4 x) > S x y) & \


496 
\ (! x y. P3 x & P2 y > S x y) & \


497 
\ (! x y. P2 x & P1 y > S x y) & \


498 
\ (! x y. P1 x & (P2 yQ1 y) > ~R x y) & \


499 
\ (! x y. P3 x & P4 y > R x y) & \


500 
\ (! x y. P3 x & P5 y > ~R x y) & \


501 
\ (! x. (P4 xP5 x) > (? y.Q0 y & R x y)) \


502 
\ > (? x y. P0 x & P0 y & (? z. Q1 z & R y z & R x y))";


503 
by (safe_meson_tac 1); (*119 secs*)

969

504 
result();


505 

1259

506 
(*The Los problem? Circulated by John Harrison*)

1465

507 
goal HOL.thy "(! x y z. P x y & P y z > P x z) & \


508 
\ (! x y z. Q x y & Q y z > Q x z) & \


509 
\ (! x y. P x y > P y x) & \


510 
\ (! (x::'a) y. P x y  Q x y) \

1259

511 
\ > (! x y. P x y)  (! x y. Q x y)";

1586

512 
by (safe_best_meson_tac 1); (*3 secs; iter. deepening is VERY slow*)

1259

513 
result();


514 


515 
(*A similar example, suggested by Johannes Schumann and credited to Pelletier*)

969

516 
goal HOL.thy "(!x y z. P x y > P y z > P x z) > \

1465

517 
\ (!x y z. Q x y > Q y z > Q x z) > \


518 
\ (!x y.Q x y > Q y x) > (!x y. P x y  Q x y) > \


519 
\ (!x y.P x y)  (!x y.Q x y)";

1586

520 
by (safe_best_meson_tac 1); (*2.7 secs*)

969

521 
result();


522 


523 
writeln"Problem 50";


524 
(*What has this to do with equality?*)


525 
goal HOL.thy "(! x. P a x  (! y.P x y)) > (? x. ! y.P x y)";


526 
by (safe_meson_tac 1);


527 
result();


528 


529 
writeln"Problem 55";


530 


531 
(*Nonequational version, from Manthey and Bry, CADE9 (Springer, 1988).


532 
meson_tac cannot report who killed Agatha. *)

1586

533 
goal HOL.thy "lives agatha & lives butler & lives charles & \

969

534 
\ (killed agatha agatha  killed butler agatha  killed charles agatha) & \


535 
\ (!x y. killed x y > hates x y & ~richer x y) & \


536 
\ (!x. hates agatha x > ~hates charles x) & \


537 
\ (hates agatha agatha & hates agatha charles) & \

1586

538 
\ (!x. lives x & ~richer x agatha > hates butler x) & \

969

539 
\ (!x. hates agatha x > hates butler x) & \


540 
\ (!x. ~hates x agatha  ~hates x butler  ~hates x charles) > \


541 
\ (? x. killed x agatha)";


542 
by (safe_meson_tac 1);


543 
result();


544 


545 
writeln"Problem 57";


546 
goal HOL.thy


547 
"P (f a b) (f b c) & P (f b c) (f a c) & \


548 
\ (! x y z. P x y & P y z > P x z) > P (f a b) (f a c)";


549 
by (safe_meson_tac 1);


550 
result();


551 


552 
writeln"Problem 58";


553 
(* Challenge found on infohol *)


554 
goal HOL.thy

1586

555 
"! P Q R x. ? v w. ! y z. P x & Q y > (P v  R w) & (R z > Q v)";

969

556 
by (safe_meson_tac 1);


557 
result();


558 


559 
writeln"Problem 59";

1586

560 
goal HOL.thy "(! x. P x = (~P(f x))) > (? x. P x & ~P(f x))";

969

561 
by (safe_meson_tac 1);


562 
result();


563 


564 
writeln"Problem 60";


565 
goal HOL.thy "! x. P x (f x) = (? y. (! z. P z y > P z (f x)) & P x y)";


566 
by (safe_meson_tac 1);


567 
result();


568 

1404

569 
writeln"Problem 62 as corrected in AAR newletter #31";


570 
goal HOL.thy

1465

571 
"(ALL x. p a & (p x > p(f x)) > p(f(f x))) = \


572 
\ (ALL x. (~ p a  p x  p(f(f x))) & \

1404

573 
\ (~ p a  ~ p(f x)  p(f(f x))))";


574 
by (safe_meson_tac 1);


575 
result();


576 

1586

577 


578 
(** Charles Morgan's problems **)


579 


580 
val axa = "! x y. T(i x(i y x))";


581 
val axb = "! x y z. T(i(i x(i y z))(i(i x y)(i x z)))";


582 
val axc = "! x y. T(i(i(n x)(n y))(i y x))";


583 
val axd = "! x y. T(i x y) & T x > T y";


584 


585 
fun axjoin ([], q) = q


586 
 axjoin (p::ps, q) = "(" ^ p ^ ") > (" ^ axjoin(ps,q) ^ ")";


587 


588 
goal HOL.thy (axjoin([axa,axb,axd], "! x. T(i x x)"));


589 
by (safe_meson_tac 1);


590 
result();


591 


592 
writeln"Problem 66";


593 
goal HOL.thy (axjoin([axa,axb,axc,axd], "! x. T(i x(n(n x)))"));


594 
(*TOO SLOW: more than 24 minutes!


595 
by (safe_meson_tac 1);


596 
result();


597 
*)


598 


599 
writeln"Problem 67";


600 
goal HOL.thy (axjoin([axa,axb,axc,axd], "! x. T(i(n(n x)) x)"));


601 
(*TOO SLOW: more than 3 minutes!


602 
by (safe_meson_tac 1);


603 
result();


604 
*)


605 


606 


607 
(*Restore original values*)


608 
Unify.trace_bound := orig_trace_bound;


609 
Unify.search_bound := orig_search_bound;


610 

969

611 
writeln"Reached end of file.";


612 


613 
(*26 August 1992: loaded in 277 secs. New Jersey v 75*)
