1459

1 
(* Title: FOLP/ex/cla

0

2 
ID: $Id$

1459

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

4 
Copyright 1993 University of Cambridge


5 

17480

6 
Classical FirstOrder Logic.

0

7 
*)


8 

17480

9 
goal (theory "FOLP") "?p : (P > Q  R) > (P>Q)  (P>R)";

0

10 
by (fast_tac FOLP_cs 1);


11 
result();


12 


13 
(*If and only if*)


14 

17480

15 
goal (theory "FOLP") "?p : (P<>Q) <> (Q<>P)";

0

16 
by (fast_tac FOLP_cs 1);


17 
result();


18 

17480

19 
goal (theory "FOLP") "?p : ~ (P <> ~P)";

0

20 
by (fast_tac FOLP_cs 1);


21 
result();


22 


23 


24 
(*Sample problems from


25 
F. J. Pelletier,


26 
SeventyFive Problems for Testing Automatic Theorem Provers,


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


28 
Errata, JAR 4 (1988), 236236.


29 


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


31 
including matrix ones  are 34 and 43.


32 
*)


33 


34 
writeln"Pelletier's examples";


35 
(*1*)

17480

36 
goal (theory "FOLP") "?p : (P>Q) <> (~Q > ~P)";

0

37 
by (fast_tac FOLP_cs 1);


38 
result();


39 


40 
(*2*)

17480

41 
goal (theory "FOLP") "?p : ~ ~ P <> P";

0

42 
by (fast_tac FOLP_cs 1);


43 
result();


44 


45 
(*3*)

17480

46 
goal (theory "FOLP") "?p : ~(P>Q) > (Q>P)";

0

47 
by (fast_tac FOLP_cs 1);


48 
result();


49 


50 
(*4*)

17480

51 
goal (theory "FOLP") "?p : (~P>Q) <> (~Q > P)";

0

52 
by (fast_tac FOLP_cs 1);


53 
result();


54 


55 
(*5*)

17480

56 
goal (theory "FOLP") "?p : ((PQ)>(PR)) > (P(Q>R))";

0

57 
by (fast_tac FOLP_cs 1);


58 
result();


59 


60 
(*6*)

17480

61 
goal (theory "FOLP") "?p : P  ~ P";

0

62 
by (fast_tac FOLP_cs 1);


63 
result();


64 


65 
(*7*)

17480

66 
goal (theory "FOLP") "?p : P  ~ ~ ~ P";

0

67 
by (fast_tac FOLP_cs 1);


68 
result();


69 


70 
(*8. Peirce's law*)

17480

71 
goal (theory "FOLP") "?p : ((P>Q) > P) > P";

0

72 
by (fast_tac FOLP_cs 1);


73 
result();


74 


75 
(*9*)

17480

76 
goal (theory "FOLP") "?p : ((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)";

0

77 
by (fast_tac FOLP_cs 1);


78 
result();


79 


80 
(*10*)

17480

81 
goal (theory "FOLP") "?p : (Q>R) & (R>P&Q) & (P>QR) > (P<>Q)";

0

82 
by (fast_tac FOLP_cs 1);


83 
result();


84 


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

17480

86 
goal (theory "FOLP") "?p : P<>P";

0

87 
by (fast_tac FOLP_cs 1);


88 
result();


89 


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

17480

91 
goal (theory "FOLP") "?p : ((P <> Q) <> R) <> (P <> (Q <> R))";

0

92 
by (fast_tac FOLP_cs 1);


93 
result();


94 


95 
(*13. Distributive law*)

17480

96 
goal (theory "FOLP") "?p : P  (Q & R) <> (P  Q) & (P  R)";

0

97 
by (fast_tac FOLP_cs 1);


98 
result();


99 


100 
(*14*)

17480

101 
goal (theory "FOLP") "?p : (P <> Q) <> ((Q  ~P) & (~QP))";

0

102 
by (fast_tac FOLP_cs 1);


103 
result();


104 


105 
(*15*)

17480

106 
goal (theory "FOLP") "?p : (P > Q) <> (~P  Q)";

0

107 
by (fast_tac FOLP_cs 1);


108 
result();


109 


110 
(*16*)

17480

111 
goal (theory "FOLP") "?p : (P>Q)  (Q>P)";

0

112 
by (fast_tac FOLP_cs 1);


113 
result();


114 


115 
(*17*)

17480

116 
goal (theory "FOLP") "?p : ((P & (Q>R))>S) <> ((~P  Q  S) & (~P  ~R  S))";

0

117 
by (fast_tac FOLP_cs 1);


118 
result();


119 


120 
writeln"Classical Logic: examples with quantifiers";


121 

17480

122 
goal (theory "FOLP") "?p : (ALL x. P(x) & Q(x)) <> (ALL x. P(x)) & (ALL x. Q(x))";

0

123 
by (fast_tac FOLP_cs 1);


124 
result();


125 

17480

126 
goal (theory "FOLP") "?p : (EX x. P>Q(x)) <> (P > (EX x. Q(x)))";

0

127 
by (fast_tac FOLP_cs 1);


128 
result();


129 

17480

130 
goal (theory "FOLP") "?p : (EX x. P(x)>Q) <> (ALL x. P(x)) > Q";

0

131 
by (fast_tac FOLP_cs 1);


132 
result();


133 

17480

134 
goal (theory "FOLP") "?p : (ALL x. P(x))  Q <> (ALL x. P(x)  Q)";

0

135 
by (fast_tac FOLP_cs 1);


136 
result();


137 


138 
writeln"Problems requiring quantifier duplication";


139 


140 
(*Needs multiple instantiation of ALL.*)


141 
(*

17480

142 
goal (theory "FOLP") "?p : (ALL x. P(x)>P(f(x))) & P(d)>P(f(f(f(d))))";

0

143 
by (best_tac FOLP_dup_cs 1);


144 
result();


145 
*)


146 
(*Needs double instantiation of the quantifier*)

17480

147 
goal (theory "FOLP") "?p : EX x. P(x) > P(a) & P(b)";

0

148 
by (best_tac FOLP_dup_cs 1);


149 
result();


150 

17480

151 
goal (theory "FOLP") "?p : EX z. P(z) > (ALL x. P(x))";

0

152 
by (best_tac FOLP_dup_cs 1);


153 
result();


154 


155 


156 
writeln"Hard examples with quantifiers";


157 


158 
writeln"Problem 18";

17480

159 
goal (theory "FOLP") "?p : EX y. ALL x. P(y)>P(x)";

0

160 
by (best_tac FOLP_dup_cs 1);


161 
result();


162 


163 
writeln"Problem 19";

17480

164 
goal (theory "FOLP") "?p : EX x. ALL y z. (P(y)>Q(z)) > (P(x)>Q(x))";

0

165 
by (best_tac FOLP_dup_cs 1);


166 
result();


167 


168 
writeln"Problem 20";

17480

169 
goal (theory "FOLP") "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)>R(z)&S(w))) \

0

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


171 
by (fast_tac FOLP_cs 1);


172 
result();


173 
(*


174 
writeln"Problem 21";

17480

175 
goal (theory "FOLP") "?p : (EX x. P>Q(x)) & (EX x. Q(x)>P) > (EX x. P<>Q(x))";

0

176 
by (best_tac FOLP_dup_cs 1);


177 
result();


178 
*)


179 
writeln"Problem 22";

17480

180 
goal (theory "FOLP") "?p : (ALL x. P <> Q(x)) > (P <> (ALL x. Q(x)))";

0

181 
by (fast_tac FOLP_cs 1);


182 
result();


183 


184 
writeln"Problem 23";

17480

185 
goal (theory "FOLP") "?p : (ALL x. P  Q(x)) <> (P  (ALL x. Q(x)))";

0

186 
by (best_tac FOLP_cs 1);


187 
result();


188 


189 
writeln"Problem 24";

17480

190 
goal (theory "FOLP") "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) > Q(x)R(x)) & \

3836

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

0

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


193 
by (fast_tac FOLP_cs 1);


194 
result();


195 
(*


196 
writeln"Problem 25";

17480

197 
goal (theory "FOLP") "?p : (EX x. P(x)) & \

0

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


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


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


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


202 
by (best_tac FOLP_cs 1);


203 
result();


204 


205 
writeln"Problem 26";

17480

206 
goal (theory "FOLP") "?u : ((EX x. p(x)) <> (EX x. q(x))) & \

1459

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

0

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


209 
by (fast_tac FOLP_cs 1);


210 
result();


211 
*)


212 
writeln"Problem 27";

17480

213 
goal (theory "FOLP") "?p : (EX x. P(x) & ~Q(x)) & \

0

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


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


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


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


218 
by (fast_tac FOLP_cs 1);


219 
result();


220 


221 
writeln"Problem 28. AMENDED";

17480

222 
goal (theory "FOLP") "?p : (ALL x. P(x) > (ALL x. Q(x))) & \

0

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

3836

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

0

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


226 
by (fast_tac FOLP_cs 1);


227 
result();


228 


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

17480

230 
goal (theory "FOLP") "?p : (EX x. P(x)) & (EX y. Q(y)) \

0

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


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


233 
by (fast_tac FOLP_cs 1);


234 
result();


235 


236 
writeln"Problem 30";

17480

237 
goal (theory "FOLP") "?p : (ALL x. P(x)  Q(x) > ~ R(x)) & \

0

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


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


240 
by (fast_tac FOLP_cs 1);


241 
result();


242 


243 
writeln"Problem 31";

17480

244 
goal (theory "FOLP") "?p : ~(EX x. P(x) & (Q(x)  R(x))) & \

0

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


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


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


248 
by (fast_tac FOLP_cs 1);


249 
result();


250 


251 
writeln"Problem 32";

17480

252 
goal (theory "FOLP") "?p : (ALL x. P(x) & (Q(x)R(x))>S(x)) & \

0

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


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


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


256 
by (best_tac FOLP_cs 1);


257 
result();


258 


259 
writeln"Problem 33";

17480

260 
goal (theory "FOLP") "?p : (ALL x. P(a) & (P(x)>P(b))>P(c)) <> \

0

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


262 
by (best_tac FOLP_cs 1);


263 
result();


264 


265 
writeln"Problem 35";

17480

266 
goal (theory "FOLP") "?p : EX x y. P(x,y) > (ALL u v. P(u,v))";

0

267 
by (best_tac FOLP_dup_cs 1);


268 
result();


269 


270 
writeln"Problem 36";

17480

271 
goal (theory "FOLP")

0

272 
"?p : (ALL x. EX y. J(x,y)) & \


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


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


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


276 
by (fast_tac FOLP_cs 1);


277 
result();


278 


279 
writeln"Problem 37";

17480

280 
goal (theory "FOLP") "?p : (ALL z. EX w. ALL x. EX y. \

3836

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

0

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


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


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


285 
by (fast_tac FOLP_cs 1);


286 
result();


287 


288 
writeln"Problem 39";

17480

289 
goal (theory "FOLP") "?p : ~ (EX x. ALL y. F(y,x) <> ~F(y,y))";

0

290 
by (fast_tac FOLP_cs 1);


291 
result();


292 


293 
writeln"Problem 40. AMENDED";

17480

294 
goal (theory "FOLP") "?p : (EX y. ALL x. F(x,y) <> F(x,x)) > \

0

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


296 
by (fast_tac FOLP_cs 1);


297 
result();


298 


299 
writeln"Problem 41";

17480

300 
goal (theory "FOLP") "?p : (ALL z. EX y. ALL x. f(x,y) <> f(x,z) & ~ f(x,x)) \

0

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


302 
by (best_tac FOLP_cs 1);


303 
result();


304 


305 
writeln"Problem 44";

17480

306 
goal (theory "FOLP") "?p : (ALL x. f(x) > \

1459

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


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

0

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


310 
by (fast_tac FOLP_cs 1);


311 
result();


312 


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


314 


315 
writeln"Problem 48";

17480

316 
goal (theory "FOLP") "?p : (a=b  c=d) & (a=c  b=d) > a=d  b=c";

0

317 
by (fast_tac FOLP_cs 1);


318 
result();


319 


320 
writeln"Problem 50";


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

17480

322 
goal (theory "FOLP") "?p : (ALL x. P(a,x)  (ALL y. P(x,y))) > (EX x. ALL y. P(x,y))";

0

323 
by (best_tac FOLP_dup_cs 1);


324 
result();


325 


326 
writeln"Problem 56";

17480

327 
goal (theory "FOLP")

0

328 
"?p : (ALL x. (EX y. P(y) & x=f(y)) > P(x)) <> (ALL x. P(x) > P(f(x)))";


329 
by (fast_tac FOLP_cs 1);


330 
result();


331 


332 
writeln"Problem 57";

17480

333 
goal (theory "FOLP")

0

334 
"?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \


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


336 
by (fast_tac FOLP_cs 1);


337 
result();


338 


339 
writeln"Problem 58 NOT PROVED AUTOMATICALLY";

17480

340 
goal (theory "FOLP") "?p : (ALL x y. f(x)=g(y)) > (ALL x y. f(f(x))=f(g(y)))";

0

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


342 
by (fast_tac (FOLP_cs addIs [f_cong]) 1);


343 
result();


344 


345 
writeln"Problem 59";

17480

346 
goal (theory "FOLP") "?p : (ALL x. P(x) <> ~P(f(x))) > (EX x. P(x) & ~P(f(x)))";

0

347 
by (best_tac FOLP_dup_cs 1);


348 
result();


349 


350 
writeln"Problem 60";

17480

351 
goal (theory "FOLP")

0

352 
"?p : ALL x. P(x,f(x)) <> (EX y. (ALL z. P(z,y) > P(z,f(x))) & P(x,y))";


353 
by (fast_tac FOLP_cs 1);


354 
result();
