author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 9841  ca3173f87b5c 
child 11451  8abfb4f7bd02 
permissions  rwrr 
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 

2059  9 
Use the "mesonlog" shell script to process logs. 
10 

1718  11 
show_hyps := false; 
969  12 

1718  13 
keep_derivs := MinDeriv; 
969  14 
by (rtac ccontr 1); 
15 
val [prem] = gethyps 1; 

16 
val nnf = make_nnf prem; 

17 
val xsko = skolemize nnf; 

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

19 
val [_,sko] = gethyps 1; 

1465  20 
val clauses = make_clauses [sko]; 
969  21 
val horns = make_horns clauses; 
1600  22 
val goes = gocls clauses; 
969  23 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

24 
Goal "False"; 
1600  25 
by (resolve_tac goes 1); 
1718  26 
keep_derivs := FullDeriv; 
1586  27 

969  28 
by (prolog_step_tac horns 1); 
1600  29 
by (iter_deepen_prolog_tac horns); 
969  30 
by (depth_prolog_tac horns); 
31 
by (best_prolog_tac size_of_subgoals horns); 

32 
*) 

33 

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

35 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

36 
context Fun.thy; 
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

37 

1586  38 
(*Deep unifications can be required, esp. during transformation to clauses*) 
39 
val orig_trace_bound = !Unify.trace_bound 

40 
and orig_search_bound = !Unify.search_bound; 

41 
Unify.trace_bound := 20; 

42 
Unify.search_bound := 40; 

43 

969  44 
(**** Interactive examples ****) 
45 

46 
(*Generate nice names for Skolem functions*) 

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

48 

49 

50 
writeln"Problem 25"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

51 
Goal "(? x. P x) & \ 
6843  52 
\ (! x. L x > ~ (M x & R x)) & \ 
53 
\ (! x. P x > (M x & L x)) & \ 

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

1586  55 
\ > (? x. Q x & P x)"; 
969  56 
by (rtac ccontr 1); 
57 
val [prem25] = gethyps 1; 

58 
val nnf25 = make_nnf prem25; 

59 
val xsko25 = skolemize nnf25; 

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

61 
val [_,sko25] = gethyps 1; 

1465  62 
val clauses25 = make_clauses [sko25]; (*7 clauses*) 
63 
val horns25 = make_horns clauses25; (*16 Horn clauses*) 

1600  64 
val go25::_ = gocls clauses25; 
969  65 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

66 
Goal "False"; 
1600  67 
by (rtac go25 1); 
969  68 
by (depth_prolog_tac horns25); 
69 

70 

71 
writeln"Problem 26"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

72 
Goal "((? x. p x) = (? x. q x)) & \ 
1586  73 
\ (! x. ! y. p x & q y > (r x = s y)) \ 
74 
\ > ((! x. p x > r x) = (! x. q x > s x))"; 

969  75 
by (rtac ccontr 1); 
76 
val [prem26] = gethyps 1; 

77 
val nnf26 = make_nnf prem26; 

78 
val xsko26 = skolemize nnf26; 

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

80 
val [_,sko26] = gethyps 1; 

1465  81 
val clauses26 = make_clauses [sko26]; (*9 clauses*) 
82 
val horns26 = make_horns clauses26; (*24 Horn clauses*) 

1600  83 
val go26::_ = gocls clauses26; 
969  84 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

85 
Goal "False"; 
1600  86 
by (rtac go26 1); 
1586  87 
by (depth_prolog_tac horns26); (*1.4 secs*) 
88 
(*Proof is of length 107!!*) 

969  89 

90 

1586  91 
writeln"Problem 43 NOW PROVED AUTOMATICALLY!!"; (*16 Horn clauses*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

92 
Goal "(! x. ! y. q x y = (! z. p z x = (p z y::bool))) \ 
6843  93 
\ > (! x. (! y. q x y = (q y x::bool)))"; 
969  94 
by (rtac ccontr 1); 
95 
val [prem43] = gethyps 1; 

96 
val nnf43 = make_nnf prem43; 

97 
val xsko43 = skolemize nnf43; 

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

99 
val [_,sko43] = gethyps 1; 

1465  100 
val clauses43 = make_clauses [sko43]; (*6*) 
101 
val horns43 = make_horns clauses43; (*16*) 

1600  102 
val go43::_ = gocls clauses43; 
969  103 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

104 
Goal "False"; 
1600  105 
by (rtac go43 1); 
1586  106 
by (best_prolog_tac size_of_subgoals horns43); (*1.6 secs*) 
107 

108 
(* 

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

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

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

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

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

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

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

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

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

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

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

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

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

122 
p (xb ?U ?V) ?U 

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

124 
p (xb ?U ?V) ?V 

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

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

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

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

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

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

131 

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

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

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

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

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

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

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

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

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

141 
*) 

969  142 

143 

144 
(*Restore variable name preservation*) 

145 
Logic.auto_rename := false; 

146 

147 

148 
(**** Batch test data ****) 

149 

150 
(*Sample problems from 

151 
F. J. Pelletier, 

152 
SeventyFive Problems for Testing Automatic Theorem Provers, 

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

154 
Errata, JAR 4 (1988), 236236. 

155 

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

157 
including matrix ones  are 34 and 43. 

158 
*) 

159 

160 
writeln"Pelletier's examples"; 

161 
(*1*) 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

162 
Goal "(P > Q) = (~Q > ~P)"; 
9841  163 
by (meson_tac 1); 
969  164 
result(); 
165 

166 
(*2*) 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

167 
Goal "(~ ~ P) = P"; 
9841  168 
by (meson_tac 1); 
969  169 
result(); 
170 

171 
(*3*) 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

172 
Goal "~(P>Q) > (Q>P)"; 
9841  173 
by (meson_tac 1); 
969  174 
result(); 
175 

176 
(*4*) 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

177 
Goal "(~P>Q) = (~Q > P)"; 
9841  178 
by (meson_tac 1); 
969  179 
result(); 
180 

181 
(*5*) 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

182 
Goal "((PQ)>(PR)) > (P(Q>R))"; 
9841  183 
by (meson_tac 1); 
969  184 
result(); 
185 

186 
(*6*) 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

187 
Goal "P  ~ P"; 
9841  188 
by (meson_tac 1); 
969  189 
result(); 
190 

191 
(*7*) 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

192 
Goal "P  ~ ~ ~ P"; 
9841  193 
by (meson_tac 1); 
969  194 
result(); 
195 

196 
(*8. Peirce's law*) 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

197 
Goal "((P>Q) > P) > P"; 
9841  198 
by (meson_tac 1); 
969  199 
result(); 
200 

201 
(*9*) 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

202 
Goal "((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)"; 
9841  203 
by (meson_tac 1); 
969  204 
result(); 
205 

206 
(*10*) 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

207 
Goal "(Q>R) & (R>P&Q) & (P>QR) > (P=Q)"; 
9841  208 
by (meson_tac 1); 
969  209 
result(); 
210 

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

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

212 
Goal "P=(P::bool)"; 
9841  213 
by (meson_tac 1); 
969  214 
result(); 
215 

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

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

217 
Goal "((P = Q) = R) = (P = (Q = R))"; 
9841  218 
by (meson_tac 1); 
969  219 
result(); 
220 

221 
(*13. Distributive law*) 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

222 
Goal "(P  (Q & R)) = ((P  Q) & (P  R))"; 
9841  223 
by (meson_tac 1); 
969  224 
result(); 
225 

226 
(*14*) 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

227 
Goal "(P = Q) = ((Q  ~P) & (~QP))"; 
9841  228 
by (meson_tac 1); 
969  229 
result(); 
230 

231 
(*15*) 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

232 
Goal "(P > Q) = (~P  Q)"; 
9841  233 
by (meson_tac 1); 
969  234 
result(); 
235 

236 
(*16*) 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

237 
Goal "(P>Q)  (Q>P)"; 
9841  238 
by (meson_tac 1); 
969  239 
result(); 
240 

241 
(*17*) 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

242 
Goal "((P & (Q>R))>S) = ((~P  Q  S) & (~P  ~R  S))"; 
9841  243 
by (meson_tac 1); 
969  244 
result(); 
245 

246 
writeln"Classical Logic: examples with quantifiers"; 

247 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

248 
Goal "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))"; 
9841  249 
by (meson_tac 1); 
969  250 
result(); 
251 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

252 
Goal "(? x. P > Q x) = (P > (? x. Q x))"; 
9841  253 
by (meson_tac 1); 
969  254 
result(); 
255 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

256 
Goal "(? x. P x > Q) = ((! x. P x) > Q)"; 
9841  257 
by (meson_tac 1); 
969  258 
result(); 
259 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

260 
Goal "((! x. P x)  Q) = (! x. P x  Q)"; 
9841  261 
by (meson_tac 1); 
969  262 
result(); 
263 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

264 
Goal "(! x. P x > P(f x)) & P d > P(f(f(f d)))"; 
9841  265 
by (meson_tac 1); 
969  266 
result(); 
267 

1259  268 
(*Needs double instantiation of EXISTS*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

269 
Goal "? x. P x > P a & P b"; 
9841  270 
by (meson_tac 1); 
969  271 
result(); 
272 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

273 
Goal "? z. P z > (! x. P x)"; 
9841  274 
by (meson_tac 1); 
969  275 
result(); 
276 

277 
writeln"Hard examples with quantifiers"; 

278 

279 
writeln"Problem 18"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

280 
Goal "? y. ! x. P y > P x"; 
9841  281 
by (meson_tac 1); 
969  282 
result(); 
283 

284 
writeln"Problem 19"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

285 
Goal "? x. ! y z. (P y > Q z) > (P x > Q x)"; 
9841  286 
by (meson_tac 1); 
969  287 
result(); 
288 

289 
writeln"Problem 20"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

290 
Goal "(! x y. ? z. ! w. (P x & Q y > R z & S w)) \ 
1586  291 
\ > (? x y. P x & Q y) > (? z. R z)"; 
9841  292 
by (meson_tac 1); 
969  293 
result(); 
294 

295 
writeln"Problem 21"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

296 
Goal "(? x. P > Q x) & (? x. Q x > P) > (? x. P=Q x)"; 
9841  297 
by (meson_tac 1); 
969  298 
result(); 
299 

300 
writeln"Problem 22"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

301 
Goal "(! x. P = Q x) > (P = (! x. Q x))"; 
9841  302 
by (meson_tac 1); 
969  303 
result(); 
304 

305 
writeln"Problem 23"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

306 
Goal "(! x. P  Q x) = (P  (! x. Q x))"; 
9841  307 
by (meson_tac 1); 
969  308 
result(); 
309 

1586  310 
writeln"Problem 24"; (*The first goal clause is useless*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

311 
Goal "~(? x. S x & Q x) & (! x. P x > Q x  R x) & \ 
6843  312 
\ (~(? x. P x) > (? x. Q x)) & (! x. Q x  R x > S x) \ 
1586  313 
\ > (? x. P x & R x)"; 
9841  314 
by (meson_tac 1); 
969  315 
result(); 
316 

317 
writeln"Problem 25"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

318 
Goal "(? x. P x) & \ 
6843  319 
\ (! x. L x > ~ (M x & R x)) & \ 
320 
\ (! x. P x > (M x & L x)) & \ 

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

1586  322 
\ > (? x. Q x & P x)"; 
9841  323 
by (meson_tac 1); 
969  324 
result(); 
325 

1586  326 
writeln"Problem 26"; (*24 Horn clauses*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

327 
Goal "((? x. p x) = (? x. q x)) & \ 
1586  328 
\ (! x. ! y. p x & q y > (r x = s y)) \ 
329 
\ > ((! x. p x > r x) = (! x. q x > s x))"; 

9841  330 
by (meson_tac 1); 
969  331 
result(); 
332 

2031  333 
writeln"Problem 27"; (*13 Horn clauses*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

334 
Goal "(? x. P x & ~Q x) & \ 
6843  335 
\ (! x. P x > R x) & \ 
336 
\ (! x. M x & L x > P x) & \ 

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

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

9841  339 
by (meson_tac 1); 
969  340 
result(); 
341 

2031  342 
writeln"Problem 28. AMENDED"; (*14 Horn clauses*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

343 
Goal "(! x. P x > (! x. Q x)) & \ 
6843  344 
\ ((! x. Q x  R x) > (? x. Q x & S x)) & \ 
345 
\ ((? x. S x) > (! x. L x > M x)) \ 

1586  346 
\ > (! x. P x & L x > M x)"; 
9841  347 
by (meson_tac 1); 
969  348 
result(); 
349 

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

2031  351 
(*62 Horn clauses*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

352 
Goal "(? x. F x) & (? y. G y) \ 
1586  353 
\ > ( ((! x. F x > H x) & (! y. G y > J y)) = \ 
354 
\ (! x y. F x & G y > H x & J y))"; 

9841  355 
by (meson_tac 1); (*0.7 secs*) 
969  356 
result(); 
357 

358 
writeln"Problem 30"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

359 
Goal "(! x. P x  Q x > ~ R x) & \ 
6843  360 
\ (! x. (Q x > ~ S x) > P x & R x) \ 
1586  361 
\ > (! x. S x)"; 
9841  362 
by (meson_tac 1); 
969  363 
result(); 
364 

1586  365 
writeln"Problem 31"; (*10 Horn clauses; first negative clauses is useless*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

366 
Goal "~(? x. P x & (Q x  R x)) & \ 
6843  367 
\ (? x. L x & P x) & \ 
368 
\ (! x. ~ R x > M x) \ 

1586  369 
\ > (? x. L x & M x)"; 
9841  370 
by (meson_tac 1); 
969  371 
result(); 
372 

373 
writeln"Problem 32"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

374 
Goal "(! x. P x & (Q x  R x)>S x) & \ 
6843  375 
\ (! x. S x & R x > L x) & \ 
376 
\ (! x. M x > R x) \ 

1586  377 
\ > (! x. P x & M x > L x)"; 
9841  378 
by (meson_tac 1); 
969  379 
result(); 
380 

1586  381 
writeln"Problem 33"; (*55 Horn clauses*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

382 
Goal "(! x. P a & (P x > P b)>P c) = \ 
6843  383 
\ (! x. (~P a  P x  P c) & (~P a  ~P b  P c))"; 
9841  384 
by (meson_tac 1); (*5.6 secs*) 
969  385 
result(); 
386 

1586  387 
writeln"Problem 34 AMENDED (TWICE!!)"; (*924 Horn clauses*) 
969  388 
(*Andrews's challenge*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

389 
Goal "((? x. ! y. p x = p y) = \ 
6843  390 
\ ((? x. q x) = (! y. p y))) = \ 
391 
\ ((? x. ! y. q x = q y) = \ 

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

9841  393 
by (meson_tac 1); (*13 secs*) 
969  394 
result(); 
395 

396 
writeln"Problem 35"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

397 
Goal "? x y. P x y > (! u v. P u v)"; 
9841  398 
by (meson_tac 1); 
969  399 
result(); 
400 

1586  401 
writeln"Problem 36"; (*15 Horn clauses*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

402 
Goal "(! x. ? y. J x y) & \ 
6843  403 
\ (! x. ? y. G x y) & \ 
404 
\ (! x y. J x y  G x y > \ 

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

969  406 
\ > (! x. ? y. H x y)"; 
9841  407 
by (meson_tac 1); 
969  408 
result(); 
409 

1586  410 
writeln"Problem 37"; (*10 Horn clauses*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

411 
Goal "(! z. ? w. ! x. ? y. \ 
3842  412 
\ (P x z > P y w) & P y z & (P y w > (? u. Q u w))) & \ 
6843  413 
\ (! x z. ~P x z > (? y. Q y z)) & \ 
414 
\ ((? x y. Q x y) > (! x. R x x)) \ 

969  415 
\ > (! x. ? y. R x y)"; 
9841  416 
by (meson_tac 1); (*causes unification tracing messages*) 
969  417 
result(); 
418 

1586  419 
writeln"Problem 38"; (*Quite hard: 422 Horn clauses!!*) 
6843  420 
Goal "(! x. p a & (p x > (? y. p y & r x y)) > \ 
1586  421 
\ (? z. ? w. p z & r x w & r w z)) = \ 
6843  422 
\ (! x. (~p a  p x  (? z. ? w. p z & r x w & r w z)) & \ 
423 
\ (~p a  ~(? y. p y & r x y)  \ 

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

1586  425 
by (safe_best_meson_tac 1); (*10 secs; iter. deepening is slightly slower*) 
969  426 
result(); 
427 

428 
writeln"Problem 39"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

429 
Goal "~ (? x. ! y. F y x = (~F y y))"; 
9841  430 
by (meson_tac 1); 
969  431 
result(); 
432 

433 
writeln"Problem 40. AMENDED"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

434 
Goal "(? y. ! x. F x y = F x x) \ 
6843  435 
\ > ~ (! x. ? y. ! z. F z y = (~F z x))"; 
9841  436 
by (meson_tac 1); 
969  437 
result(); 
438 

439 
writeln"Problem 41"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

440 
Goal "(! z. (? y. (! x. f x y = (f x z & ~ f x x)))) \ 
6843  441 
\ > ~ (? z. ! x. f x z)"; 
9841  442 
by (meson_tac 1); 
969  443 
result(); 
444 

445 
writeln"Problem 42"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

446 
Goal "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))"; 
9841  447 
by (meson_tac 1); 
969  448 
result(); 
449 

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

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

451 
Goal "(! x. ! y. q x y = (! z. p z x = (p z y::bool))) \ 
6843  452 
\ > (! x. (! y. q x y = (q y x::bool)))"; 
2031  453 
by (safe_best_meson_tac 1); 
1586  454 
(*1.6 secs; iter. deepening is slightly slower*) 
969  455 
result(); 
456 

1586  457 
writeln"Problem 44"; (*13 Horn clauses; 7step proof*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

458 
Goal "(! x. f x > \ 
6843  459 
\ (? y. g y & h x y & (? y. g y & ~ h x y))) & \ 
460 
\ (? x. j x & (! y. g y > h x y)) \ 

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

9841  462 
by (meson_tac 1); 
969  463 
result(); 
464 

1586  465 
writeln"Problem 45"; (*27 Horn clauses; 54step proof*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

466 
Goal "(! x. f x & (! y. g y & h x y > j x y) \ 
6843  467 
\ > (! y. g y & h x y > k y)) & \ 
1586  468 
\ ~ (? y. l y & k y) & \ 
469 
\ (? x. f x & (! y. h x y > l y) \ 

6843  470 
\ & (! y. g y & h x y > j x y)) \ 
1586  471 
\ > (? x. f x & ~ (? y. g y & h x y))"; 
2031  472 
by (safe_best_meson_tac 1); 
1586  473 
(*1.6 secs; iter. deepening is slightly slower*) 
474 
result(); 

475 

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

6843  477 
Goal "(! x. f x & (! y. f y & h y x > g y) > g x) & \ 
478 
\ ((? x. f x & ~g x) > \ 

1586  479 
\ (? x. f x & ~g x & (! y. f y & ~g y > j x y))) & \ 
6843  480 
\ (! x y. f x & f y & h x y > ~j y x) \ 
1586  481 
\ > (! x. f x > g x)"; 
2031  482 
by (safe_best_meson_tac 1); 
1586  483 
(*1.7 secs; iter. deepening is slightly slower*) 
969  484 
result(); 
485 

1586  486 
writeln"Problem 47. Schubert's Steamroller"; 
6843  487 
(*26 clauses; 63 Horn clauses 
488 
87094 inferences so far. Searching to depth 36*) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

9092  506 
by (safe_best_meson_tac 1); (*MUCH faster than iterative deepening*) 
969  507 
result(); 
508 

1259  509 
(*The Los problem? Circulated by John Harrison*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

510 
Goal "(! x y z. P x y & P y z > P x z) & \ 
6843  511 
\ (! x y z. Q x y & Q y z > Q x z) & \ 
512 
\ (! x y. P x y > P y x) & \ 

513 
\ (! x y. P x y  Q x y) \ 

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

2615  515 
by (safe_best_meson_tac 1); (*2.3 secs; iter. deepening is VERY slow*) 
1259  516 
result(); 
517 

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

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

519 
Goal "(!x y z. P x y > P y z > P x z) > \ 
6843  520 
\ (!x y z. Q x y > Q y z > Q x z) > \ 
521 
\ (!x y. Q x y > Q y x) > (!x y. P x y  Q x y) > \ 

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

1586  523 
by (safe_best_meson_tac 1); (*2.7 secs*) 
969  524 
result(); 
525 

526 
writeln"Problem 50"; 

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

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

528 
Goal "(! x. P a x  (! y. P x y)) > (? x. ! y. P x y)"; 
9841  529 
by (meson_tac 1); 
969  530 
result(); 
531 

532 
writeln"Problem 55"; 

533 

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

535 
meson_tac cannot report who killed Agatha. *) 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

536 
Goal "lives agatha & lives butler & lives charles & \ 
6843  537 
\ (killed agatha agatha  killed butler agatha  killed charles agatha) & \ 
538 
\ (!x y. killed x y > hates x y & ~richer x y) & \ 

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

540 
\ (hates agatha agatha & hates agatha charles) & \ 

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

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

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

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

9841  545 
by (meson_tac 1); 
969  546 
result(); 
547 

548 
writeln"Problem 57"; 

6843  549 
Goal "P (f a b) (f b c) & P (f b c) (f a c) & \ 
550 
\ (! x y z. P x y & P y z > P x z) > P (f a b) (f a c)"; 

9841  551 
by (meson_tac 1); 
969  552 
result(); 
553 

554 
writeln"Problem 58"; 

555 
(* Challenge found on infohol *) 

6843  556 
Goal "! P Q R x. ? v w. ! y z. P x & Q y > (P v  R w) & (R z > Q v)"; 
9841  557 
by (meson_tac 1); 
969  558 
result(); 
559 

560 
writeln"Problem 59"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

561 
Goal "(! x. P x = (~P(f x))) > (? x. P x & ~P(f x))"; 
9841  562 
by (meson_tac 1); 
969  563 
result(); 
564 

565 
writeln"Problem 60"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

566 
Goal "! x. P x (f x) = (? y. (! z. P z y > P z (f x)) & P x y)"; 
9841  567 
by (meson_tac 1); 
969  568 
result(); 
569 

2715  570 
writeln"Problem 62 as corrected in JAR 18 (1997), page 135"; 
6843  571 
Goal "(ALL x. p a & (p x > p(f x)) > p(f(f x))) = \ 
572 
\ (ALL x. (~ p a  p x  p(f(f x))) & \ 

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

9841  574 
by (meson_tac 1); 
1404  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 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

588 
Goal (axjoin([axa,axb,axd], "! x. T(i x x)")); 
9841  589 
by (meson_tac 1); 
1586  590 
result(); 
591 

592 
writeln"Problem 66"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

593 
Goal (axjoin([axa,axb,axc,axd], "! x. T(i x(n(n x)))")); 
7183  594 
(*TOO SLOW, several minutes! 
595 
208346 inferences so far. Searching to depth 23 

9841  596 
by (meson_tac 1); 
1586  597 
result(); 
598 
*) 

599 

600 
writeln"Problem 67"; 

5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

601 
Goal (axjoin([axa,axb,axc,axd], "! x. T(i(n(n x)) x)")); 
1586  602 
(*TOO SLOW: more than 3 minutes! 
6843  603 
51061 inferences so far. Searching to depth 21 
9841  604 
by (meson_tac 1); 
1586  605 
result(); 
606 
*) 

607 

608 

609 
(*Restore original values*) 

610 
Unify.trace_bound := orig_trace_bound; 

611 
Unify.search_bound := orig_search_bound; 

612 

969  613 
writeln"Reached end of file."; 
614 

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