author  paulson 
Fri, 14 Aug 1998 12:02:35 +0200  
changeset 5317  3a9214482762 
parent 3842  b55686a7b22c 
child 6843  eeeddde75f3f 
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) & \ 
1586  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)) \ 

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))) \ 
969  93 
\ > (! x. (! y. q x y = (q y x::bool)))"; 
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)"; 
969  163 
by (safe_meson_tac 1); 
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"; 
969  168 
by (safe_meson_tac 1); 
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)"; 
969  173 
by (safe_meson_tac 1); 
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)"; 
969  178 
by (safe_meson_tac 1); 
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))"; 
969  183 
by (safe_meson_tac 1); 
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"; 
969  188 
by (safe_meson_tac 1); 
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"; 
969  193 
by (safe_meson_tac 1); 
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"; 
969  198 
by (safe_meson_tac 1); 
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)"; 
969  203 
by (safe_meson_tac 1); 
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)"; 
969  208 
by (safe_meson_tac 1); 
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)"; 
969  213 
by (safe_meson_tac 1); 
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))"; 
1586  218 
by (safe_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))"; 
969  223 
by (safe_meson_tac 1); 
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))"; 
969  228 
by (safe_meson_tac 1); 
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)"; 
969  233 
by (safe_meson_tac 1); 
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)"; 
969  238 
by (safe_meson_tac 1); 
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))"; 
969  243 
by (safe_meson_tac 1); 
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))"; 
969  249 
by (safe_meson_tac 1); 
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))"; 
969  253 
by (safe_meson_tac 1); 
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)"; 
969  257 
by (safe_meson_tac 1); 
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)"; 
969  261 
by (safe_meson_tac 1); 
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)))"; 
969  265 
by (safe_meson_tac 1); 
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"; 
969  270 
by (safe_meson_tac 1); 
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)"; 
969  274 
by (safe_meson_tac 1); 
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"; 
969  281 
by (safe_meson_tac 1); 
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)"; 
969  286 
by (safe_meson_tac 1); 
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)"; 
969  292 
by (safe_meson_tac 1); 
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)"; 
969  297 
by (safe_meson_tac 1); 
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))"; 
969  302 
by (safe_meson_tac 1); 
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))"; 
969  307 
by (safe_meson_tac 1); 
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) & \ 
3842  312 
\ (~(? x. P x) > (? x. Q x)) & (! x. Q x  R x > S x) \ 
1586  313 
\ > (? x. P x & R x)"; 
969  314 
by (safe_meson_tac 1); 
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) & \ 
1586  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)) \ 

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

969  323 
by (safe_meson_tac 1); 
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))"; 

969  330 
by (safe_meson_tac 1); 
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) & \ 
1586  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)"; 

969  339 
by (safe_meson_tac 1); 
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)) & \ 
1586  344 
\ ((! x. Q x  R x) > (? x. Q x & S x)) & \ 
3842  345 
\ ((? x. S x) > (! x. L x > M x)) \ 
1586  346 
\ > (! x. P x & L x > M x)"; 
969  347 
by (safe_meson_tac 1); 
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))"; 

355 
by (safe_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) & \ 
1586  360 
\ (! x. (Q x > ~ S x) > P x & R x) \ 
361 
\ > (! x. S x)"; 

969  362 
by (safe_meson_tac 1); 
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)) & \ 
1586  367 
\ (? x. L x & P x) & \ 
368 
\ (! x. ~ R x > M x) \ 

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

969  370 
by (safe_meson_tac 1); 
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) & \ 
1586  375 
\ (! x. S x & R x > L x) & \ 
376 
\ (! x. M x > R x) \ 

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

969  378 
by (safe_meson_tac 1); 
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) = \ 
1586  383 
\ (! x. (~P a  P x  P c) & (~P a  ~P b  P c))"; 
1465  384 
by (safe_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) = \ 
1586  390 
\ ((? x. q x) = (! y. p y))) = \ 
391 
\ ((? x. ! y. q x = q y) = \ 

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

393 
by (safe_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)"; 
969  398 
by (safe_meson_tac 1); 
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) & \ 
969  403 
\ (! x. ? y. G x y) & \ 
1465  404 
\ (! x y. J x y  G x y > \ 
969  405 
\ (! z. J y z  G y z > H x z)) \ 
406 
\ > (! x. ? y. H x y)"; 

407 
by (safe_meson_tac 1); 

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))) & \ 
969  413 
\ (! x z. ~P x z > (? y. Q y z)) & \ 
414 
\ ((? x y. Q x y) > (! x. R x x)) \ 

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

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

417 
result(); 

418 

1586  419 
writeln"Problem 38"; (*Quite hard: 422 Horn clauses!!*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

420 
Goal 
1586  421 
"(! x. p a & (p x > (? y. p y & r x y)) > \ 
422 
\ (? z. ? w. p z & r x w & r w z)) = \ 

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

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

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

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

969  427 
result(); 
428 

429 
writeln"Problem 39"; 

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

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

433 

434 
writeln"Problem 40. AMENDED"; 

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

435 
Goal "(? y. ! x. F x y = F x x) \ 
969  436 
\ > ~ (! x. ? y. ! z. F z y = (~F z x))"; 
437 
by (safe_meson_tac 1); 

438 
result(); 

439 

440 
writeln"Problem 41"; 

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

441 
Goal "(! z. (? y. (! x. f x y = (f x z & ~ f x x)))) \ 
969  442 
\ > ~ (? z. ! x. f x z)"; 
443 
by (safe_meson_tac 1); 

444 
result(); 

445 

446 
writeln"Problem 42"; 

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

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

450 

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

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

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

1586  458 
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

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

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

969  463 
by (safe_meson_tac 1); 
464 
result(); 

465 

1586  466 
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

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

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

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

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

2031  473 
by (safe_best_meson_tac 1); 
1586  474 
(*1.6 secs; iter. deepening is slightly slower*) 
475 
result(); 

476 

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

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

478 
Goal 
1586  479 
"(! x. f x & (! y. f y & h y x > g y) > g x) & \ 
3842  480 
\ ((? x. f x & ~g x) > \ 
1586  481 
\ (? x. f x & ~g x & (! y. f y & ~g y > j x y))) & \ 
482 
\ (! x y. f x & f y & h x y > ~j y x) \ 

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

2031  484 
by (safe_best_meson_tac 1); 
1586  485 
(*1.7 secs; iter. deepening is slightly slower*) 
969  486 
result(); 
487 

1586  488 
writeln"Problem 47. Schubert's Steamroller"; 
2031  489 
(*26 clauses; 63 Horn clauses*) 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

490 
Goal 
3842  491 
"(! x. P1 x > P0 x) & (? x. P1 x) & \ 
492 
\ (! x. P2 x > P0 x) & (? x. P2 x) & \ 

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

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

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

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

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

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

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

1586  500 
\ (! x y. P3 y & (P5 xP4 x) > S x y) & \ 
501 
\ (! x y. P3 x & P2 y > S x y) & \ 

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

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

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

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

3842  506 
\ (! x. (P4 xP5 x) > (? y. Q0 y & R x y)) \ 
1586  507 
\ > (? x y. P0 x & P0 y & (? z. Q1 z & R y z & R x y))"; 
2031  508 
by (safe_meson_tac 1); (*119 secs*) 
969  509 
result(); 
510 

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

512 
Goal "(! x y z. P x y & P y z > P x z) & \ 
2615  513 
\ (! x y z. Q x y & Q y z > Q x z) & \ 
514 
\ (! x y. P x y > P y x) & \ 

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

1259  516 
\ > (! x y. P x y)  (! x y. Q x y)"; 
2615  517 
by (safe_best_meson_tac 1); (*2.3 secs; iter. deepening is VERY slow*) 
1259  518 
result(); 
519 

520 
(*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

521 
Goal "(!x y z. P x y > P y z > P x z) > \ 
1465  522 
\ (!x y z. Q x y > Q y z > Q x z) > \ 
3842  523 
\ (!x y. Q x y > Q y x) > (!x y. P x y  Q x y) > \ 
524 
\ (!x y. P x y)  (!x y. Q x y)"; 

1586  525 
by (safe_best_meson_tac 1); (*2.7 secs*) 
969  526 
result(); 
527 

528 
writeln"Problem 50"; 

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

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

530 
Goal "(! x. P a x  (! y. P x y)) > (? x. ! y. P x y)"; 
969  531 
by (safe_meson_tac 1); 
532 
result(); 

533 

534 
writeln"Problem 55"; 

535 

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

537 
meson_tac cannot report who killed Agatha. *) 

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

538 
Goal "lives agatha & lives butler & lives charles & \ 
969  539 
\ (killed agatha agatha  killed butler agatha  killed charles agatha) & \ 
540 
\ (!x y. killed x y > hates x y & ~richer x y) & \ 

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

542 
\ (hates agatha agatha & hates agatha charles) & \ 

1586  543 
\ (!x. lives x & ~richer x agatha > hates butler x) & \ 
969  544 
\ (!x. hates agatha x > hates butler x) & \ 
545 
\ (!x. ~hates x agatha  ~hates x butler  ~hates x charles) > \ 

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

547 
by (safe_meson_tac 1); 

548 
result(); 

549 

550 
writeln"Problem 57"; 

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

551 
Goal 
969  552 
"P (f a b) (f b c) & P (f b c) (f a c) & \ 
553 
\ (! x y z. P x y & P y z > P x z) > P (f a b) (f a c)"; 

554 
by (safe_meson_tac 1); 

555 
result(); 

556 

557 
writeln"Problem 58"; 

558 
(* Challenge found on infohol *) 

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

559 
Goal 
1586  560 
"! P Q R x. ? v w. ! y z. P x & Q y > (P v  R w) & (R z > Q v)"; 
969  561 
by (safe_meson_tac 1); 
562 
result(); 

563 

564 
writeln"Problem 59"; 

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

565 
Goal "(! x. P x = (~P(f x))) > (? x. P x & ~P(f x))"; 
969  566 
by (safe_meson_tac 1); 
567 
result(); 

568 

569 
writeln"Problem 60"; 

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

570 
Goal "! x. P x (f x) = (? y. (! z. P z y > P z (f x)) & P x y)"; 
969  571 
by (safe_meson_tac 1); 
572 
result(); 

573 

2715  574 
writeln"Problem 62 as corrected in JAR 18 (1997), page 135"; 
5317
3a9214482762
Uses Goal instead of "goal...thy" to avoid theory problems
paulson
parents:
3842
diff
changeset

575 
Goal 
1465  576 
"(ALL x. p a & (p x > p(f x)) > p(f(f x))) = \ 
577 
\ (ALL x. (~ p a  p x  p(f(f x))) & \ 

1404  578 
\ (~ p a  ~ p(f x)  p(f(f x))))"; 
579 
by (safe_meson_tac 1); 

580 
result(); 

581 

1586  582 

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

584 

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

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

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

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

589 

590 
fun axjoin ([], q) = q 

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

592 

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

593 
Goal (axjoin([axa,axb,axd], "! x. T(i x x)")); 
1586  594 
by (safe_meson_tac 1); 
595 
result(); 

596 

597 
writeln"Problem 66"; 

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

598 
Goal (axjoin([axa,axb,axc,axd], "! x. T(i x(n(n x)))")); 
1586  599 
(*TOO SLOW: more than 24 minutes! 
600 
by (safe_meson_tac 1); 

601 
result(); 

602 
*) 

603 

604 
writeln"Problem 67"; 

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

605 
Goal (axjoin([axa,axb,axc,axd], "! x. T(i(n(n x)) x)")); 
1586  606 
(*TOO SLOW: more than 3 minutes! 
607 
by (safe_meson_tac 1); 

608 
result(); 

609 
*) 

610 

611 

612 
(*Restore original values*) 

613 
Unify.trace_bound := orig_trace_bound; 

614 
Unify.search_bound := orig_search_bound; 

615 

969  616 
writeln"Reached end of file."; 
617 

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