author  lcp 
Fri, 24 Sep 1993 11:27:15 +0200  
changeset 13  b73f7e42135e 
parent 0  a5a9c433f639 
child 36  70c6014c9b6f 
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 

165 
(*from Vladimir Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 123*) 

166 
goal FOL.thy "EX x x'. ALL y. EX z z'. \ 

167 
\ (~P(y,y)  P(x,x)  ~S(z,x)) & \ 

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

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

170 

171 
writeln"Hard examples with quantifiers"; 

172 

173 
writeln"Problem 18"; 

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

175 
by (best_tac FOL_dup_cs 1); 

176 
result(); 

177 

178 
writeln"Problem 19"; 

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

180 
by (best_tac FOL_dup_cs 1); 

181 
result(); 

182 

183 
writeln"Problem 20"; 

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

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

186 
by (fast_tac FOL_cs 1); 

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

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

189 
by (fast_tac FOL_cs 1); 

190 
result(); 

191 

192 
writeln"Problem 21"; 

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

194 
by (best_tac FOL_dup_cs 1); 

195 
result(); 

196 

197 
writeln"Problem 22"; 

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

199 
by (fast_tac FOL_cs 1); 

200 
result(); 

201 

202 
writeln"Problem 23"; 

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

204 
by (best_tac FOL_cs 1); 

205 
result(); 

206 

207 
writeln"Problem 24"; 

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

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

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

211 
by (fast_tac FOL_cs 1); 

212 
result(); 

213 

214 
writeln"Problem 25"; 

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

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

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

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

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

220 
by (best_tac FOL_cs 1); 

221 
(*slow*) 

222 
result(); 

223 

224 
writeln"Problem 26"; 

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

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

228 
by (fast_tac FOL_cs 1); 

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

237 
by (fast_tac FOL_cs 1); 

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

245 
by (fast_tac FOL_cs 1); 

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

252 
by (fast_tac FOL_cs 1); 

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

259 
by (fast_tac FOL_cs 1); 

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

267 
by (fast_tac FOL_cs 1); 

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

275 
by (best_tac FOL_cs 1); 

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

281 
by (best_tac FOL_cs 1); 

282 
result(); 

283 

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

285 
(*Andrews's challenge*) 

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

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

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

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

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

293 
result(); 

294 

295 
writeln"Problem 35"; 

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

297 
by (best_tac FOL_dup_cs 1); 

298 
(*6.1 secs*) 

299 
result(); 

300 

301 
writeln"Problem 36"; 

302 
goal FOL.thy 

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

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

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

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

307 
by (fast_tac FOL_cs 1); 

308 
result(); 

309 

310 
writeln"Problem 37"; 

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

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

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

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

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

316 
by (fast_tac FOL_cs 1); 

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

318 
result(); 

319 

320 
writeln"Problem 38. NOT PROVED"; 

321 
goal FOL.thy 

322 
"(ALL x. p(a) & (p(x) > (EX y. p(y) & r(x,y))) > \ 

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

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

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

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

327 

328 
writeln"Problem 39"; 

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

330 
by (fast_tac FOL_cs 1); 

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

336 
by (fast_tac FOL_cs 1); 

337 
result(); 

338 

339 
writeln"Problem 41"; 

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

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

342 
by (best_tac FOL_cs 1); 

343 
result(); 

344 

345 
writeln"Problem 42 NOT PROVED"; 

346 
goal FOL.thy "~ (EX y. ALL x. p(x,y) <> ~ (EX z. p(x,z) & p(z,x)))"; 

347 

348 
writeln"Problem 43 NOT PROVED AUTOMATICALLY"; 

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

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

351 

352 

353 
writeln"Problem 44"; 

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

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

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

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

358 
by (fast_tac FOL_cs 1); 

359 
result(); 

360 

361 
writeln"Problem 45"; 

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

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

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

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

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

367 
\ > (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))"; 

368 
by (best_tac FOL_cs 1); 

369 
(*41.5 secs*) 

370 
result(); 

371 

372 

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

374 

375 
writeln"Problem 48"; 

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

377 
by (fast_tac FOL_cs 1); 

378 
result(); 

379 

380 
writeln"Problem 49 NOT PROVED AUTOMATICALLY"; 

381 
(*Hard because it involves substitution for Vars; 

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

383 
goal FOL.thy "(EX x y::'a. ALL z. z=x  z=y) & P(a) & P(b) & (~a=b) \ 

384 
\ > (ALL u::'a.P(u))"; 

385 
by (safe_tac FOL_cs); 

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

387 
ba 1; 

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

389 
ba 1; 

390 
by (fast_tac FOL_cs 1); 

391 
result(); 

392 

393 
writeln"Problem 50"; 

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

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

396 
by (best_tac FOL_dup_cs 1); 

397 
result(); 

398 

399 
writeln"Problem 51"; 

400 
goal FOL.thy 

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

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

403 
by (fast_tac FOL_cs 1); 

404 
result(); 

405 

406 
writeln"Problem 52"; 

407 
(*Almost the same as 51. *) 

408 
goal FOL.thy 

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

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

411 
by (best_tac FOL_cs 1); 

412 
result(); 

413 

414 
writeln"Problem 55"; 

415 

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

417 
goal FOL.thy 

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

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

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

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

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

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

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

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

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

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

428 
\ ~ agatha=butler > \ 

429 
\ killed(?who,agatha)"; 

430 
by (safe_tac FOL_cs); 

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

432 
ba 1; 

433 
be (spec RS exE) 1; 

434 
by (REPEAT (etac allE 1)); 

435 
by (fast_tac FOL_cs 1); 

436 
result(); 

437 
****) 

438 

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

440 
fast_tac DISCOVERS who killed Agatha. *) 

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

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

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

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

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

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

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

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

449 
\ killed(?who,agatha)"; 

450 
by (fast_tac FOL_cs 1); 

451 
result(); 

452 

453 

454 
writeln"Problem 56"; 

455 
goal FOL.thy 

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

457 
by (fast_tac FOL_cs 1); 

458 
result(); 

459 

460 
writeln"Problem 57"; 

461 
goal FOL.thy 

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

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

464 
by (fast_tac FOL_cs 1); 

465 
result(); 

466 

467 
writeln"Problem 58 NOT PROVED AUTOMATICALLY"; 

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

469 
val f_cong = read_instantiate [("t","f")] subst_context; 

470 
by (fast_tac (FOL_cs addIs [f_cong]) 1); 

471 
result(); 

472 

473 
writeln"Problem 59"; 

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

475 
by (best_tac FOL_dup_cs 1); 

476 
result(); 

477 

478 
writeln"Problem 60"; 

479 
goal FOL.thy 

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

481 
by (fast_tac FOL_cs 1); 

482 
result(); 

483 

484 

485 
writeln"Reached end of file."; 

486 

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