author  paulson 
Fri, 14 Feb 1997 10:36:33 +0100  
changeset 2614  0b1364481214 
parent 2601  b301958c465d 
child 2715  79c35a051196 
permissions  rwrr 
1462  1 
(* Title: FOL/ex/cla.ML 
0  2 
ID: $Id$ 
1459  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
665
97e9ad6c1c4a
FOL/ex/cla: proofs now use deepen_tac instead of best_tac FOL_dup_cs
lcp
parents:
644
diff
changeset

4 
Copyright 1994 University of Cambridge 
0  5 

6 
Classical FirstOrder Logic 

7 
*) 

8 

1462  9 
writeln"File FOL/ex/cla.ML"; 
0  10 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2574
diff
changeset

11 
open Cla; (*in case structure IntPr is open!*) 
0  12 

13 
goal FOL.thy "(P > Q  R) > (P>Q)  (P>R)"; 

2469  14 
by (Fast_tac 1); 
0  15 
result(); 
16 

17 
(*If and only if*) 

18 

19 
goal FOL.thy "(P<>Q) <> (Q<>P)"; 

2469  20 
by (Fast_tac 1); 
0  21 
result(); 
22 

23 
goal FOL.thy "~ (P <> ~P)"; 

2469  24 
by (Fast_tac 1); 
0  25 
result(); 
26 

27 

28 
(*Sample problems from 

29 
F. J. Pelletier, 

30 
SeventyFive Problems for Testing Automatic Theorem Provers, 

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

32 
Errata, JAR 4 (1988), 236236. 

33 

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

35 
including matrix ones  are 34 and 43. 

36 
*) 

37 

38 
writeln"Pelletier's examples"; 

39 
(*1*) 

40 
goal FOL.thy "(P>Q) <> (~Q > ~P)"; 

2469  41 
by (Fast_tac 1); 
0  42 
result(); 
43 

44 
(*2*) 

45 
goal FOL.thy "~ ~ P <> P"; 

2469  46 
by (Fast_tac 1); 
0  47 
result(); 
48 

49 
(*3*) 

50 
goal FOL.thy "~(P>Q) > (Q>P)"; 

2469  51 
by (Fast_tac 1); 
0  52 
result(); 
53 

54 
(*4*) 

55 
goal FOL.thy "(~P>Q) <> (~Q > P)"; 

2469  56 
by (Fast_tac 1); 
0  57 
result(); 
58 

59 
(*5*) 

60 
goal FOL.thy "((PQ)>(PR)) > (P(Q>R))"; 

2469  61 
by (Fast_tac 1); 
0  62 
result(); 
63 

64 
(*6*) 

65 
goal FOL.thy "P  ~ P"; 

2469  66 
by (Fast_tac 1); 
0  67 
result(); 
68 

69 
(*7*) 

70 
goal FOL.thy "P  ~ ~ ~ P"; 

2469  71 
by (Fast_tac 1); 
0  72 
result(); 
73 

74 
(*8. Peirce's law*) 

75 
goal FOL.thy "((P>Q) > P) > P"; 

2469  76 
by (Fast_tac 1); 
0  77 
result(); 
78 

79 
(*9*) 

80 
goal FOL.thy "((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)"; 

2469  81 
by (Fast_tac 1); 
0  82 
result(); 
83 

84 
(*10*) 

85 
goal FOL.thy "(Q>R) & (R>P&Q) & (P>QR) > (P<>Q)"; 

2469  86 
by (Fast_tac 1); 
0  87 
result(); 
88 

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

90 
goal FOL.thy "P<>P"; 

2469  91 
by (Fast_tac 1); 
0  92 
result(); 
93 

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

95 
goal FOL.thy "((P <> Q) <> R) <> (P <> (Q <> R))"; 

2469  96 
by (Fast_tac 1); 
0  97 
result(); 
98 

99 
(*13. Distributive law*) 

100 
goal FOL.thy "P  (Q & R) <> (P  Q) & (P  R)"; 

2469  101 
by (Fast_tac 1); 
0  102 
result(); 
103 

104 
(*14*) 

105 
goal FOL.thy "(P <> Q) <> ((Q  ~P) & (~QP))"; 

2469  106 
by (Fast_tac 1); 
0  107 
result(); 
108 

109 
(*15*) 

110 
goal FOL.thy "(P > Q) <> (~P  Q)"; 

2469  111 
by (Fast_tac 1); 
0  112 
result(); 
113 

114 
(*16*) 

115 
goal FOL.thy "(P>Q)  (Q>P)"; 

2469  116 
by (Fast_tac 1); 
0  117 
result(); 
118 

119 
(*17*) 

120 
goal FOL.thy "((P & (Q>R))>S) <> ((~P  Q  S) & (~P  ~R  S))"; 

2469  121 
by (Fast_tac 1); 
0  122 
result(); 
123 

124 
writeln"Classical Logic: examples with quantifiers"; 

125 

126 
goal FOL.thy "(ALL x. P(x) & Q(x)) <> (ALL x. P(x)) & (ALL x. Q(x))"; 

2469  127 
by (Fast_tac 1); 
0  128 
result(); 
129 

130 
goal FOL.thy "(EX x. P>Q(x)) <> (P > (EX x.Q(x)))"; 

2469  131 
by (Fast_tac 1); 
0  132 
result(); 
133 

134 
goal FOL.thy "(EX x.P(x)>Q) <> (ALL x.P(x)) > Q"; 

2469  135 
by (Fast_tac 1); 
0  136 
result(); 
137 

138 
goal FOL.thy "(ALL x.P(x))  Q <> (ALL x. P(x)  Q)"; 

2469  139 
by (Fast_tac 1); 
0  140 
result(); 
141 

13
b73f7e42135e
Added example from Avron: GentzenType Systems, Resolution and Tableaux, JAR 10
lcp
parents:
0
diff
changeset

142 
(*Discussed in Avron, GentzenType Systems, Resolution and Tableaux, 
b73f7e42135e
Added example from Avron: GentzenType Systems, Resolution and Tableaux, JAR 10
lcp
parents:
0
diff
changeset

143 
JAR 10 (265281), 1993. Proof is trivial!*) 
b73f7e42135e
Added example from Avron: GentzenType Systems, Resolution and Tableaux, JAR 10
lcp
parents:
0
diff
changeset

144 
goal FOL.thy 
b73f7e42135e
Added example from Avron: GentzenType Systems, Resolution and Tableaux, JAR 10
lcp
parents:
0
diff
changeset

145 
"~ ((EX x.~P(x)) & ((EX x.P(x))  (EX x.P(x) & Q(x))) & ~ (EX x.P(x)))"; 
2469  146 
by (Fast_tac 1); 
13
b73f7e42135e
Added example from Avron: GentzenType Systems, Resolution and Tableaux, JAR 10
lcp
parents:
0
diff
changeset

147 
result(); 
b73f7e42135e
Added example from Avron: GentzenType Systems, Resolution and Tableaux, JAR 10
lcp
parents:
0
diff
changeset

148 

0  149 
writeln"Problems requiring quantifier duplication"; 
150 

151 
(*Needs multiple instantiation of ALL.*) 

152 
goal FOL.thy "(ALL x. P(x)>P(f(x))) & P(d)>P(f(f(f(d))))"; 

2469  153 
by (Deepen_tac 0 1); 
0  154 
result(); 
155 

156 
(*Needs double instantiation of the quantifier*) 

157 
goal FOL.thy "EX x. P(x) > P(a) & P(b)"; 

2469  158 
by (Deepen_tac 0 1); 
0  159 
result(); 
160 

161 
goal FOL.thy "EX z. P(z) > (ALL x. P(x))"; 

2469  162 
by (Deepen_tac 0 1); 
0  163 
result(); 
164 

492  165 
goal FOL.thy "EX x. (EX y. P(y)) > P(x)"; 
2469  166 
by (Deepen_tac 0 1); 
492  167 
result(); 
168 

665
97e9ad6c1c4a
FOL/ex/cla: proofs now use deepen_tac instead of best_tac FOL_dup_cs
lcp
parents:
644
diff
changeset

169 
(*V. Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 123. NOT PROVED*) 
0  170 
goal FOL.thy "EX x x'. ALL y. EX z z'. \ 
171 
\ (~P(y,y)  P(x,x)  ~S(z,x)) & \ 

172 
\ (S(x,y)  ~S(y,z)  Q(z',z')) & \ 

173 
\ (Q(x',y)  ~Q(y,z')  S(x',x'))"; 

174 

175 
writeln"Hard examples with quantifiers"; 

176 

177 
writeln"Problem 18"; 

178 
goal FOL.thy "EX y. ALL x. P(y)>P(x)"; 

2469  179 
by (Deepen_tac 0 1); 
0  180 
result(); 
181 

182 
writeln"Problem 19"; 

183 
goal FOL.thy "EX x. ALL y z. (P(y)>Q(z)) > (P(x)>Q(x))"; 

2469  184 
by (Deepen_tac 0 1); 
0  185 
result(); 
186 

187 
writeln"Problem 20"; 

188 
goal FOL.thy "(ALL x y. EX z. ALL w. (P(x)&Q(y)>R(z)&S(w))) \ 

189 
\ > (EX x y. P(x) & Q(y)) > (EX z. R(z))"; 

2469  190 
by (Fast_tac 1); 
0  191 
result(); 
192 

193 
writeln"Problem 21"; 

194 
goal FOL.thy "(EX x. P>Q(x)) & (EX x. Q(x)>P) > (EX x. P<>Q(x))"; 

2469  195 
by (Deepen_tac 0 1); 
0  196 
result(); 
197 

198 
writeln"Problem 22"; 

199 
goal FOL.thy "(ALL x. P <> Q(x)) > (P <> (ALL x. Q(x)))"; 

2469  200 
by (Fast_tac 1); 
0  201 
result(); 
202 

203 
writeln"Problem 23"; 

204 
goal FOL.thy "(ALL x. P  Q(x)) <> (P  (ALL x. Q(x)))"; 

2469  205 
by (Best_tac 1); 
0  206 
result(); 
207 

208 
writeln"Problem 24"; 

209 
goal FOL.thy "~(EX x. S(x)&Q(x)) & (ALL x. P(x) > Q(x)R(x)) & \ 

2574  210 
\ (~(EX x.P(x)) > (EX x.Q(x))) & (ALL x. Q(x)R(x) > S(x)) \ 
0  211 
\ > (EX x. P(x)&R(x))"; 
2469  212 
by (Fast_tac 1); 
0  213 
result(); 
214 

215 
writeln"Problem 25"; 

216 
goal FOL.thy "(EX x. P(x)) & \ 

217 
\ (ALL x. L(x) > ~ (M(x) & R(x))) & \ 

218 
\ (ALL x. P(x) > (M(x) & L(x))) & \ 

219 
\ ((ALL x. P(x)>Q(x))  (EX x. P(x)&R(x))) \ 

220 
\ > (EX x. Q(x)&P(x))"; 

2469  221 
by (Best_tac 1); 
0  222 
result(); 
223 

224 
writeln"Problem 26"; 

1459  225 
goal FOL.thy "((EX x. p(x)) <> (EX x. q(x))) & \ 
226 
\ (ALL x. ALL y. p(x) & q(y) > (r(x) <> s(y))) \ 

0  227 
\ > ((ALL x. p(x)>r(x)) <> (ALL x. q(x)>s(x)))"; 
2469  228 
by (Fast_tac 1); 
0  229 
result(); 
230 

231 
writeln"Problem 27"; 

232 
goal FOL.thy "(EX x. P(x) & ~Q(x)) & \ 

233 
\ (ALL x. P(x) > R(x)) & \ 

234 
\ (ALL x. M(x) & L(x) > P(x)) & \ 

235 
\ ((EX x. R(x) & ~ Q(x)) > (ALL x. L(x) > ~ R(x))) \ 

236 
\ > (ALL x. M(x) > ~L(x))"; 

2469  237 
by (Fast_tac 1); 
0  238 
result(); 
239 

240 
writeln"Problem 28. AMENDED"; 

241 
goal FOL.thy "(ALL x. P(x) > (ALL x. Q(x))) & \ 

242 
\ ((ALL x. Q(x)R(x)) > (EX x. Q(x)&S(x))) & \ 

243 
\ ((EX x.S(x)) > (ALL x. L(x) > M(x))) \ 

244 
\ > (ALL x. P(x) & L(x) > M(x))"; 

2469  245 
by (Fast_tac 1); 
0  246 
result(); 
247 

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

249 
goal FOL.thy "(EX x. P(x)) & (EX y. Q(y)) \ 

250 
\ > ((ALL x. P(x)>R(x)) & (ALL y. Q(y)>S(y)) <> \ 

251 
\ (ALL x y. P(x) & Q(y) > R(x) & S(y)))"; 

2469  252 
by (Fast_tac 1); 
0  253 
result(); 
254 

255 
writeln"Problem 30"; 

256 
goal FOL.thy "(ALL x. P(x)  Q(x) > ~ R(x)) & \ 

257 
\ (ALL x. (Q(x) > ~ S(x)) > P(x) & R(x)) \ 

258 
\ > (ALL x. S(x))"; 

2469  259 
by (Fast_tac 1); 
0  260 
result(); 
261 

262 
writeln"Problem 31"; 

263 
goal FOL.thy "~(EX x.P(x) & (Q(x)  R(x))) & \ 

264 
\ (EX x. L(x) & P(x)) & \ 

265 
\ (ALL x. ~ R(x) > M(x)) \ 

266 
\ > (EX x. L(x) & M(x))"; 

2469  267 
by (Fast_tac 1); 
0  268 
result(); 
269 

270 
writeln"Problem 32"; 

271 
goal FOL.thy "(ALL x. P(x) & (Q(x)R(x))>S(x)) & \ 

272 
\ (ALL x. S(x) & R(x) > L(x)) & \ 

273 
\ (ALL x. M(x) > R(x)) \ 

274 
\ > (ALL x. P(x) & M(x) > L(x))"; 

2469  275 
by (Best_tac 1); 
0  276 
result(); 
277 

278 
writeln"Problem 33"; 

279 
goal FOL.thy "(ALL x. P(a) & (P(x)>P(b))>P(c)) <> \ 

280 
\ (ALL x. (~P(a)  P(x)  P(c)) & (~P(a)  ~P(b)  P(c)))"; 

2469  281 
by (Best_tac 1); 
0  282 
result(); 
283 

665
97e9ad6c1c4a
FOL/ex/cla: proofs now use deepen_tac instead of best_tac FOL_dup_cs
lcp
parents:
644
diff
changeset

284 
writeln"Problem 34 AMENDED (TWICE!!)"; 
0  285 
(*Andrews's challenge*) 
1459  286 
goal FOL.thy "((EX x. ALL y. p(x) <> p(y)) <> \ 
287 
\ ((EX x. q(x)) <> (ALL y. p(y)))) <> \ 

288 
\ ((EX x. ALL y. q(x) <> q(y)) <> \ 

0  289 
\ ((EX x. p(x)) <> (ALL y. q(y))))"; 
2469  290 
by (Deepen_tac 0 1); 
0  291 
result(); 
292 

293 
writeln"Problem 35"; 

294 
goal FOL.thy "EX x y. P(x,y) > (ALL u v. P(u,v))"; 

732  295 
by (mini_tac 1); 
2469  296 
by (Fast_tac 1); 
665
97e9ad6c1c4a
FOL/ex/cla: proofs now use deepen_tac instead of best_tac FOL_dup_cs
lcp
parents:
644
diff
changeset

297 
(*Without miniscope, would have to use deepen_tac; would be slower*) 
0  298 
result(); 
299 

300 
writeln"Problem 36"; 

301 
goal FOL.thy 

302 
"(ALL x. EX y. J(x,y)) & \ 

303 
\ (ALL x. EX y. G(x,y)) & \ 

304 
\ (ALL x y. J(x,y)  G(x,y) > (ALL z. J(y,z)  G(y,z) > H(x,z))) \ 

305 
\ > (ALL x. EX y. H(x,y))"; 

2469  306 
by (Fast_tac 1); 
0  307 
result(); 
308 

309 
writeln"Problem 37"; 

310 
goal FOL.thy "(ALL z. EX w. ALL x. EX y. \ 

311 
\ (P(x,z)>P(y,w)) & P(y,z) & (P(y,w) > (EX u.Q(u,w)))) & \ 

312 
\ (ALL x z. ~P(x,z) > (EX y. Q(y,z))) & \ 

313 
\ ((EX x y. Q(x,y)) > (ALL x. R(x,x))) \ 

314 
\ > (ALL x. EX y. R(x,y))"; 

2469  315 
by (Fast_tac 1); 
0  316 
result(); 
317 

428  318 
writeln"Problem 38"; 
0  319 
goal FOL.thy 
1459  320 
"(ALL x. p(a) & (p(x) > (EX y. p(y) & r(x,y))) > \ 
321 
\ (EX z. EX w. p(z) & r(x,w) & r(w,z))) <> \ 

322 
\ (ALL x. (~p(a)  p(x)  (EX z. EX w. p(z) & r(x,w) & r(w,z))) & \ 

323 
\ (~p(a)  ~(EX y. p(y) & r(x,y))  \ 

0  324 
\ (EX z. EX w. p(z) & r(x,w) & r(w,z))))"; 
2469  325 
by (Deepen_tac 0 1); (*beats fast_tac!*) 
665
97e9ad6c1c4a
FOL/ex/cla: proofs now use deepen_tac instead of best_tac FOL_dup_cs
lcp
parents:
644
diff
changeset

326 
result(); 
0  327 

328 
writeln"Problem 39"; 

329 
goal FOL.thy "~ (EX x. ALL y. F(y,x) <> ~F(y,y))"; 

2469  330 
by (Fast_tac 1); 
0  331 
result(); 
332 

333 
writeln"Problem 40. AMENDED"; 

334 
goal FOL.thy "(EX y. ALL x. F(x,y) <> F(x,x)) > \ 

335 
\ ~(ALL x. EX y. ALL z. F(z,y) <> ~ F(z,x))"; 

2469  336 
by (Fast_tac 1); 
0  337 
result(); 
338 

339 
writeln"Problem 41"; 

1459  340 
goal FOL.thy "(ALL z. EX y. ALL x. f(x,y) <> f(x,z) & ~ f(x,x)) \ 
0  341 
\ > ~ (EX z. ALL x. f(x,z))"; 
2469  342 
by (Fast_tac 1); 
0  343 
result(); 
344 

428  345 
writeln"Problem 42"; 
0  346 
goal FOL.thy "~ (EX y. ALL x. p(x,y) <> ~ (EX z. p(x,z) & p(z,x)))"; 
2469  347 
by (Deepen_tac 0 1); 
428  348 
result(); 
0  349 

732  350 
writeln"Problem 43"; 
1459  351 
goal FOL.thy "(ALL x. ALL y. q(x,y) <> (ALL z. p(z,x) <> p(z,y))) \ 
665
97e9ad6c1c4a
FOL/ex/cla: proofs now use deepen_tac instead of best_tac FOL_dup_cs
lcp
parents:
644
diff
changeset

352 
\ > (ALL x. ALL y. q(x,y) <> q(y,x))"; 
2469  353 
by (Auto_tac()); 
354 
(*The proof above cheats by using rewriting! A purely logical proof is 

355 
by (mini_tac 1 THEN Deepen_tac 5 1); 

1809  356 
Can use just deepen_tac but it requires 253 secs?!? 
2469  357 
by (Deepen_tac 0 1); 
732  358 
*) 
665
97e9ad6c1c4a
FOL/ex/cla: proofs now use deepen_tac instead of best_tac FOL_dup_cs
lcp
parents:
644
diff
changeset

359 
result(); 
0  360 

361 
writeln"Problem 44"; 

1459  362 
goal FOL.thy "(ALL x. f(x) > \ 
363 
\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \ 

364 
\ (EX x. j(x) & (ALL y. g(y) > h(x,y))) \ 

0  365 
\ > (EX x. j(x) & ~f(x))"; 
2469  366 
by (Fast_tac 1); 
0  367 
result(); 
368 

369 
writeln"Problem 45"; 

1459  370 
goal FOL.thy "(ALL x. f(x) & (ALL y. g(y) & h(x,y) > j(x,y)) \ 
371 
\ > (ALL y. g(y) & h(x,y) > k(y))) & \ 

372 
\ ~ (EX y. l(y) & k(y)) & \ 

373 
\ (EX x. f(x) & (ALL y. h(x,y) > l(y)) \ 

374 
\ & (ALL y. g(y) & h(x,y) > j(x,y))) \ 

0  375 
\ > (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))"; 
2469  376 
by (Best_tac 1); 
0  377 
result(); 
378 

379 

380 
writeln"Problems (mainly) involving equality or functions"; 

381 

382 
writeln"Problem 48"; 

383 
goal FOL.thy "(a=b  c=d) & (a=c  b=d) > a=d  b=c"; 

2469  384 
by (Fast_tac 1); 
0  385 
result(); 
386 

387 
writeln"Problem 49 NOT PROVED AUTOMATICALLY"; 

388 
(*Hard because it involves substitution for Vars; 

389 
the type constraint ensures that x,y,z have the same type as a,b,u. *) 

36  390 
goal FOL.thy "(EX x y::'a. ALL z. z=x  z=y) & P(a) & P(b) & a~=b \ 
1459  391 
\ > (ALL u::'a.P(u))"; 
2469  392 
by (Step_tac 1); 
0  393 
by (res_inst_tac [("x","a")] allE 1); 
1459  394 
by (assume_tac 1); 
0  395 
by (res_inst_tac [("x","b")] allE 1); 
1459  396 
by (assume_tac 1); 
2469  397 
by (Fast_tac 1); 
0  398 
result(); 
399 

400 
writeln"Problem 50"; 

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

402 
goal FOL.thy "(ALL x. P(a,x)  (ALL y.P(x,y))) > (EX x. ALL y.P(x,y))"; 

732  403 
by (mini_tac 1); 
2469  404 
by (Deepen_tac 0 1); 
0  405 
result(); 
406 

407 
writeln"Problem 51"; 

408 
goal FOL.thy 

409 
"(EX z w. ALL x y. P(x,y) <> (x=z & y=w)) > \ 

410 
\ (EX z. ALL x. EX w. (ALL y. P(x,y) <> y=w) <> x=z)"; 

2469  411 
by (Fast_tac 1); 
0  412 
result(); 
413 

414 
writeln"Problem 52"; 

415 
(*Almost the same as 51. *) 

416 
goal FOL.thy 

417 
"(EX z w. ALL x y. P(x,y) <> (x=z & y=w)) > \ 

418 
\ (EX w. ALL y. EX z. (ALL x. P(x,y) <> x=z) <> y=w)"; 

2469  419 
by (Best_tac 1); 
0  420 
result(); 
421 

422 
writeln"Problem 55"; 

423 

424 
(*Original, equational version by Len Schubert, via Pelletier *** NOT PROVED 

425 
goal FOL.thy 

426 
"(EX x. lives(x) & killed(x,agatha)) & \ 

427 
\ lives(agatha) & lives(butler) & lives(charles) & \ 

428 
\ (ALL x. lives(x) > x=agatha  x=butler  x=charles) & \ 

429 
\ (ALL x y. killed(x,y) > hates(x,y)) & \ 

430 
\ (ALL x y. killed(x,y) > ~richer(x,y)) & \ 

431 
\ (ALL x. hates(agatha,x) > ~hates(charles,x)) & \ 

432 
\ (ALL x. ~ x=butler > hates(agatha,x)) & \ 

433 
\ (ALL x. ~richer(x,agatha) > hates(butler,x)) & \ 

434 
\ (ALL x. hates(agatha,x) > hates(butler,x)) & \ 

435 
\ (ALL x. EX y. ~hates(x,y)) & \ 

436 
\ ~ agatha=butler > \ 

437 
\ killed(?who,agatha)"; 

2469  438 
by (Step_tac 1); 
0  439 
by (dres_inst_tac [("x1","x")] (spec RS mp) 1); 
1459  440 
by (assume_tac 1); 
441 
by (etac (spec RS exE) 1); 

0  442 
by (REPEAT (etac allE 1)); 
2469  443 
by (Fast_tac 1); 
0  444 
result(); 
445 
****) 

446 

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

448 
fast_tac DISCOVERS who killed Agatha. *) 

449 
goal FOL.thy "lives(agatha) & lives(butler) & lives(charles) & \ 

450 
\ (killed(agatha,agatha)  killed(butler,agatha)  killed(charles,agatha)) & \ 

451 
\ (ALL x y. killed(x,y) > hates(x,y) & ~richer(x,y)) & \ 

452 
\ (ALL x. hates(agatha,x) > ~hates(charles,x)) & \ 

453 
\ (hates(agatha,agatha) & hates(agatha,charles)) & \ 

454 
\ (ALL x. lives(x) & ~richer(x,agatha) > hates(butler,x)) & \ 

455 
\ (ALL x. hates(agatha,x) > hates(butler,x)) & \ 

456 
\ (ALL x. ~hates(x,agatha)  ~hates(x,butler)  ~hates(x,charles)) > \ 

457 
\ killed(?who,agatha)"; 

2469  458 
by (Fast_tac 1); 
0  459 
result(); 
460 

461 

462 
writeln"Problem 56"; 

463 
goal FOL.thy 

464 
"(ALL x. (EX y. P(y) & x=f(y)) > P(x)) <> (ALL x. P(x) > P(f(x)))"; 

2469  465 
by (Fast_tac 1); 
0  466 
result(); 
467 

468 
writeln"Problem 57"; 

469 
goal FOL.thy 

470 
"P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \ 

471 
\ (ALL x y z. P(x,y) & P(y,z) > P(x,z)) > P(f(a,b), f(a,c))"; 

2469  472 
by (Fast_tac 1); 
0  473 
result(); 
474 

475 
writeln"Problem 58 NOT PROVED AUTOMATICALLY"; 

476 
goal FOL.thy "(ALL x y. f(x)=g(y)) > (ALL x y. f(f(x))=f(g(y)))"; 

2469  477 
by (slow_tac (!claset addEs [subst_context]) 1); 
0  478 
result(); 
479 

480 
writeln"Problem 59"; 

481 
goal FOL.thy "(ALL x. P(x) <> ~P(f(x))) > (EX x. P(x) & ~P(f(x)))"; 

2469  482 
by (Deepen_tac 0 1); 
0  483 
result(); 
484 

485 
writeln"Problem 60"; 

486 
goal FOL.thy 

487 
"ALL x. P(x,f(x)) <> (EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))"; 

2469  488 
by (Fast_tac 1); 
0  489 
result(); 
490 

1404  491 
writeln"Problem 62 as corrected in AAR newletter #31"; 
492 
goal FOL.thy 

1459  493 
"(ALL x. p(a) & (p(x) > p(f(x))) > p(f(f(x)))) <> \ 
494 
\ (ALL x. (~p(a)  p(x)  p(f(f(x)))) & \ 

1404  495 
\ (~p(a)  ~p(f(x))  p(f(f(x)))))"; 
2469  496 
by (Fast_tac 1); 
1404  497 
result(); 
498 

1560  499 
(*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.) 
500 
author U. Egly*) 

501 
goal FOL.thy 

502 
"((EX X. a(X) & (ALL Y. c(Y) > (ALL Z. d(X, Y, Z)))) > \ 

503 
\ (EX W. c(W) & (ALL Y. c(Y) > (ALL Z. d(W, Y, Z))))) \ 

504 
\ & \ 

505 
\ (ALL W. c(W) & (ALL U. c(U) > (ALL V. d(W, U, V))) > \ 

506 
\ (ALL Y Z. \ 

507 
\ (c(Y) & h2(Y, Z) > h3(W, Y, Z) & o(W, g)) & \ 

508 
\ (c(Y) & ~h2(Y, Z) > h3(W, Y, Z) & o(W, b)))) \ 

509 
\ & \ 

510 
\ (ALL W. c(W) & \ 

511 
\ (ALL Y Z. \ 

512 
\ (c(Y) & h2(Y, Z) > h3(W, Y, Z) & o(W, g)) & \ 

513 
\ (c(Y) & ~h2(Y, Z) > h3(W, Y, Z) & o(W, b))) > \ 

514 
\ (EX V. c(V) & \ 

515 
\ (ALL Y. ((c(Y) & h3(W, Y, Y)) & o(W, g) > ~h2(V, Y)) & \ 

516 
\ ((c(Y) & h3(W, Y, Y)) & o(W, b) > h2(V, Y) & o(V, b))))) \ 

517 
\ > \ 

518 
\ ~ (EX X. a(X) & (ALL Y. c(Y) > (ALL Z. d(X, Y, Z))))"; 

519 

0  520 

2614  521 
(* Challenge found on infohol *) 
522 
goal FOL.thy 

523 
"ALL x. EX v w. ALL y z. P(x) & Q(y) > (P(v)  R(w)) & (R(z) > Q(v))"; 

524 
by (Deepen_tac 0 1); 

525 
result(); 

526 

0  527 
writeln"Reached end of file."; 
528 

732  529 
(*Thu Jul 23 1992: loaded in 467s using iffE [on SPARC2] *) 
530 
(*Mon Nov 14 1994: loaded in 144s [on SPARC10, with deepen_tac] *) 

531 
(*Wed Nov 16 1994: loaded in 138s [after addition of norm_term_skip] *) 

532 
(*Mon Nov 21 1994: loaded in 131s [DEPTH_FIRST suppressing repetitions] *) 

533 