author  lcp 
Wed, 19 Oct 1994 09:41:48 +0100  
changeset 644  112cf8574cf1 
parent 492  7bc980c7585e 
child 665  97e9ad6c1c4a 
permissions  rwrr 
0  1 
(* Title: FOL/ex/cla 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1992 University of Cambridge 

5 

6 
Classical FirstOrder Logic 

7 
*) 

8 

9 
writeln"File FOL/ex/cla."; 

10 

11 
open Cla; (*in case structure Int is open!*) 

12 

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

14 
by (fast_tac FOL_cs 1); 

15 
result(); 

16 

17 
(*If and only if*) 

18 

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

20 
by (fast_tac FOL_cs 1); 

21 
result(); 

22 

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

24 
by (fast_tac FOL_cs 1); 

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)"; 

41 
by (fast_tac FOL_cs 1); 

42 
result(); 

43 

44 
(*2*) 

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

46 
by (fast_tac FOL_cs 1); 

47 
result(); 

48 

49 
(*3*) 

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

51 
by (fast_tac FOL_cs 1); 

52 
result(); 

53 

54 
(*4*) 

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

56 
by (fast_tac FOL_cs 1); 

57 
result(); 

58 

59 
(*5*) 

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

61 
by (fast_tac FOL_cs 1); 

62 
result(); 

63 

64 
(*6*) 

65 
goal FOL.thy "P  ~ P"; 

66 
by (fast_tac FOL_cs 1); 

67 
result(); 

68 

69 
(*7*) 

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

71 
by (fast_tac FOL_cs 1); 

72 
result(); 

73 

74 
(*8. Peirce's law*) 

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

76 
by (fast_tac FOL_cs 1); 

77 
result(); 

78 

79 
(*9*) 

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

81 
by (fast_tac FOL_cs 1); 

82 
result(); 

83 

84 
(*10*) 

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

86 
by (fast_tac FOL_cs 1); 

87 
result(); 

88 

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

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

91 
by (fast_tac FOL_cs 1); 

92 
result(); 

93 

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

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

96 
by (fast_tac FOL_cs 1); 

97 
result(); 

98 

99 
(*13. Distributive law*) 

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

101 
by (fast_tac FOL_cs 1); 

102 
result(); 

103 

104 
(*14*) 

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

106 
by (fast_tac FOL_cs 1); 

107 
result(); 

108 

109 
(*15*) 

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

111 
by (fast_tac FOL_cs 1); 

112 
result(); 

113 

114 
(*16*) 

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

116 
by (fast_tac FOL_cs 1); 

117 
result(); 

118 

119 
(*17*) 

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

121 
by (fast_tac FOL_cs 1); 

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))"; 

127 
by (fast_tac FOL_cs 1); 

128 
result(); 

129 

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

131 
by (fast_tac FOL_cs 1); 

132 
result(); 

133 

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

135 
by (fast_tac FOL_cs 1); 

136 
result(); 

137 

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

139 
by (fast_tac FOL_cs 1); 

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)))"; 
b73f7e42135e
Added example from Avron: GentzenType Systems, Resolution and Tableaux, JAR 10
lcp
parents:
0
diff
changeset

146 
by (fast_tac FOL_cs 1); 
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))))"; 

153 
by (best_tac FOL_dup_cs 1); 

154 
result(); 

155 

156 
(*Needs double instantiation of the quantifier*) 

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

158 
by (best_tac FOL_dup_cs 1); 

159 
result(); 

160 

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

162 
by (best_tac FOL_dup_cs 1); 

163 
result(); 

164 

492  165 
goal FOL.thy "EX x. (EX y. P(y)) > P(x)"; 
166 
by (best_tac FOL_dup_cs 1); 

167 
result(); 

168 

0  169 
(*from Vladimir Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 123*) 
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)"; 

179 
by (best_tac FOL_dup_cs 1); 

180 
result(); 

181 

182 
writeln"Problem 19"; 

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

184 
by (best_tac FOL_dup_cs 1); 

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))"; 

190 
by (fast_tac FOL_cs 1); 

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))"; 

195 
by (best_tac FOL_dup_cs 1); 

196 
result(); 

197 

198 
writeln"Problem 22"; 

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

200 
by (fast_tac FOL_cs 1); 

201 
result(); 

202 

203 
writeln"Problem 23"; 

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

205 
by (best_tac FOL_cs 1); 

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)) & \ 

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

211 
\ > (EX x. P(x)&R(x))"; 

212 
by (fast_tac FOL_cs 1); 

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))"; 

221 
by (best_tac FOL_cs 1); 

222 
(*slow*) 

223 
result(); 

224 

225 
writeln"Problem 26"; 

226 
goal FOL.thy "((EX x. p(x)) <> (EX x. q(x))) & \ 

227 
\ (ALL x. ALL y. p(x) & q(y) > (r(x) <> s(y))) \ 

228 
\ > ((ALL x. p(x)>r(x)) <> (ALL x. q(x)>s(x)))"; 

229 
by (fast_tac FOL_cs 1); 

230 
result(); 

231 

232 
writeln"Problem 27"; 

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

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

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

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

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

238 
by (fast_tac FOL_cs 1); 

239 
result(); 

240 

241 
writeln"Problem 28. AMENDED"; 

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

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

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

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

246 
by (fast_tac FOL_cs 1); 

247 
result(); 

248 

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

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

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

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

253 
by (fast_tac FOL_cs 1); 

254 
result(); 

255 

256 
writeln"Problem 30"; 

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

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

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

260 
by (fast_tac FOL_cs 1); 

261 
result(); 

262 

263 
writeln"Problem 31"; 

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

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

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

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

268 
by (fast_tac FOL_cs 1); 

269 
result(); 

270 

271 
writeln"Problem 32"; 

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

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

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

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

276 
by (best_tac FOL_cs 1); 

277 
result(); 

278 

279 
writeln"Problem 33"; 

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

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

282 
by (best_tac FOL_cs 1); 

283 
result(); 

284 

285 
writeln"Problem 34 AMENDED (TWICE!!) NOT PROVED AUTOMATICALLY"; 

286 
(*Andrews's challenge*) 

287 
goal FOL.thy "((EX x. ALL y. p(x) <> p(y)) <> \ 

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

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

290 
\ ((EX x. p(x)) <> (ALL y. q(y))))"; 

291 
by (safe_tac FOL_cs); (*22 secs*) 

292 
by (TRYALL (fast_tac FOL_cs)); (*128 secs*) 

293 
by (TRYALL (best_tac FOL_dup_cs)); (*77 secs*) 

294 
result(); 

295 

296 
writeln"Problem 35"; 

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

298 
by (best_tac FOL_dup_cs 1); 

299 
(*6.1 secs*) 

300 
result(); 

301 

302 
writeln"Problem 36"; 

303 
goal FOL.thy 

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

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

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

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

308 
by (fast_tac FOL_cs 1); 

309 
result(); 

310 

311 
writeln"Problem 37"; 

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

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

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

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

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

317 
by (fast_tac FOL_cs 1); 

318 
(*slow...Poly/ML: 9.7 secs*) 

319 
result(); 

320 

428  321 
writeln"Problem 38"; 
0  322 
goal FOL.thy 
323 
"(ALL x. p(a) & (p(x) > (EX y. p(y) & r(x,y))) > \ 

324 
\ (EX z. EX w. p(z) & r(x,w) & r(w,z))) <> \ 

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

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

327 
\ (EX z. EX w. p(z) & r(x,w) & r(w,z))))"; 

428  328 
by (fast_tac FOL_cs 1); 
0  329 

330 
writeln"Problem 39"; 

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

332 
by (fast_tac FOL_cs 1); 

333 
result(); 

334 

335 
writeln"Problem 40. AMENDED"; 

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

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

338 
by (fast_tac FOL_cs 1); 

339 
result(); 

340 

341 
writeln"Problem 41"; 

342 
goal FOL.thy "(ALL z. EX y. ALL x. f(x,y) <> f(x,z) & ~ f(x,x)) \ 

343 
\ > ~ (EX z. ALL x. f(x,z))"; 

344 
by (best_tac FOL_cs 1); 

345 
result(); 

346 

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

0  351 

352 
writeln"Problem 43 NOT PROVED AUTOMATICALLY"; 

353 
goal FOL.thy "(ALL x. ALL y. q(x,y) <> (ALL z. p(z,x) <> p(z,y))) \ 

354 
\ > (ALL x. (ALL y. q(x,y) <> q(y,x)))"; 

355 

356 
writeln"Problem 44"; 

357 
goal FOL.thy "(ALL x. f(x) > \ 

358 
\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \ 

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

360 
\ > (EX x. j(x) & ~f(x))"; 

361 
by (fast_tac FOL_cs 1); 

362 
result(); 

363 

364 
writeln"Problem 45"; 

365 
goal FOL.thy "(ALL x. f(x) & (ALL y. g(y) & h(x,y) > j(x,y)) \ 

366 
\ > (ALL y. g(y) & h(x,y) > k(y))) & \ 

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

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

36  369 
\ & (ALL y. g(y) & h(x,y) > j(x,y))) \ 
0  370 
\ > (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))"; 
371 
by (best_tac FOL_cs 1); 

372 
result(); 

373 

374 

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

376 

377 
writeln"Problem 48"; 

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

379 
by (fast_tac FOL_cs 1); 

380 
result(); 

381 

382 
writeln"Problem 49 NOT PROVED AUTOMATICALLY"; 

383 
(*Hard because it involves substitution for Vars; 

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

36  385 
goal FOL.thy "(EX x y::'a. ALL z. z=x  z=y) & P(a) & P(b) & a~=b \ 
0  386 
\ > (ALL u::'a.P(u))"; 
387 
by (safe_tac FOL_cs); 

388 
by (res_inst_tac [("x","a")] allE 1); 

389 
ba 1; 

390 
by (res_inst_tac [("x","b")] allE 1); 

391 
ba 1; 

392 
by (fast_tac FOL_cs 1); 

393 
result(); 

394 

395 
writeln"Problem 50"; 

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

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

398 
by (best_tac FOL_dup_cs 1); 

399 
result(); 

400 

401 
writeln"Problem 51"; 

402 
goal FOL.thy 

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

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

405 
by (fast_tac FOL_cs 1); 

406 
result(); 

407 

408 
writeln"Problem 52"; 

409 
(*Almost the same as 51. *) 

410 
goal FOL.thy 

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

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

413 
by (best_tac FOL_cs 1); 

414 
result(); 

415 

416 
writeln"Problem 55"; 

417 

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

419 
goal FOL.thy 

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

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

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

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

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

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

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

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

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

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

430 
\ ~ agatha=butler > \ 

431 
\ killed(?who,agatha)"; 

432 
by (safe_tac FOL_cs); 

433 
by (dres_inst_tac [("x1","x")] (spec RS mp) 1); 

434 
ba 1; 

435 
be (spec RS exE) 1; 

436 
by (REPEAT (etac allE 1)); 

437 
by (fast_tac FOL_cs 1); 

438 
result(); 

439 
****) 

440 

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

442 
fast_tac DISCOVERS who killed Agatha. *) 

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

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

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

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

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

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

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

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

451 
\ killed(?who,agatha)"; 

452 
by (fast_tac FOL_cs 1); 

453 
result(); 

454 

455 

456 
writeln"Problem 56"; 

457 
goal FOL.thy 

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

459 
by (fast_tac FOL_cs 1); 

460 
result(); 

461 

462 
writeln"Problem 57"; 

463 
goal FOL.thy 

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

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

466 
by (fast_tac FOL_cs 1); 

467 
result(); 

468 

469 
writeln"Problem 58 NOT PROVED AUTOMATICALLY"; 

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

644  471 
by (fast_tac (FOL_cs addEs [subst_context]) 1); 
0  472 
result(); 
473 

474 
writeln"Problem 59"; 

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

476 
by (best_tac FOL_dup_cs 1); 

477 
result(); 

478 

479 
writeln"Problem 60"; 

480 
goal FOL.thy 

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

482 
by (fast_tac FOL_cs 1); 

483 
result(); 

484 

485 

486 
writeln"Reached end of file."; 

487 

488 
(*Thu Jul 23 1992: loaded in 467.1s using iffE*) 