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 


6 
Classical FirstOrder Logic


7 
*)


8 

1464

9 
writeln"File FOLP/ex/cla.ML";

0

10 


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


12 


13 
goal FOLP.thy "?p : (P > Q  R) > (P>Q)  (P>R)";


14 
by (fast_tac FOLP_cs 1);


15 
result();


16 


17 
(*If and only if*)


18 


19 
goal FOLP.thy "?p : (P<>Q) <> (Q<>P)";


20 
by (fast_tac FOLP_cs 1);


21 
result();


22 


23 
goal FOLP.thy "?p : ~ (P <> ~P)";


24 
by (fast_tac FOLP_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 FOLP.thy "?p : (P>Q) <> (~Q > ~P)";


41 
by (fast_tac FOLP_cs 1);


42 
result();


43 


44 
(*2*)


45 
goal FOLP.thy "?p : ~ ~ P <> P";


46 
by (fast_tac FOLP_cs 1);


47 
result();


48 


49 
(*3*)


50 
goal FOLP.thy "?p : ~(P>Q) > (Q>P)";


51 
by (fast_tac FOLP_cs 1);


52 
result();


53 


54 
(*4*)


55 
goal FOLP.thy "?p : (~P>Q) <> (~Q > P)";


56 
by (fast_tac FOLP_cs 1);


57 
result();


58 


59 
(*5*)


60 
goal FOLP.thy "?p : ((PQ)>(PR)) > (P(Q>R))";


61 
by (fast_tac FOLP_cs 1);


62 
result();


63 


64 
(*6*)


65 
goal FOLP.thy "?p : P  ~ P";


66 
by (fast_tac FOLP_cs 1);


67 
result();


68 


69 
(*7*)


70 
goal FOLP.thy "?p : P  ~ ~ ~ P";


71 
by (fast_tac FOLP_cs 1);


72 
result();


73 


74 
(*8. Peirce's law*)


75 
goal FOLP.thy "?p : ((P>Q) > P) > P";


76 
by (fast_tac FOLP_cs 1);


77 
result();


78 


79 
(*9*)


80 
goal FOLP.thy "?p : ((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)";


81 
by (fast_tac FOLP_cs 1);


82 
result();


83 


84 
(*10*)


85 
goal FOLP.thy "?p : (Q>R) & (R>P&Q) & (P>QR) > (P<>Q)";


86 
by (fast_tac FOLP_cs 1);


87 
result();


88 


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


90 
goal FOLP.thy "?p : P<>P";


91 
by (fast_tac FOLP_cs 1);


92 
result();


93 


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


95 
goal FOLP.thy "?p : ((P <> Q) <> R) <> (P <> (Q <> R))";


96 
by (fast_tac FOLP_cs 1);


97 
result();


98 


99 
(*13. Distributive law*)


100 
goal FOLP.thy "?p : P  (Q & R) <> (P  Q) & (P  R)";


101 
by (fast_tac FOLP_cs 1);


102 
result();


103 


104 
(*14*)


105 
goal FOLP.thy "?p : (P <> Q) <> ((Q  ~P) & (~QP))";


106 
by (fast_tac FOLP_cs 1);


107 
result();


108 


109 
(*15*)


110 
goal FOLP.thy "?p : (P > Q) <> (~P  Q)";


111 
by (fast_tac FOLP_cs 1);


112 
result();


113 


114 
(*16*)


115 
goal FOLP.thy "?p : (P>Q)  (Q>P)";


116 
by (fast_tac FOLP_cs 1);


117 
result();


118 


119 
(*17*)


120 
goal FOLP.thy "?p : ((P & (Q>R))>S) <> ((~P  Q  S) & (~P  ~R  S))";


121 
by (fast_tac FOLP_cs 1);


122 
result();


123 


124 
writeln"Classical Logic: examples with quantifiers";


125 


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


127 
by (fast_tac FOLP_cs 1);


128 
result();


129 


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


131 
by (fast_tac FOLP_cs 1);


132 
result();


133 


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


135 
by (fast_tac FOLP_cs 1);


136 
result();


137 


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


139 
by (fast_tac FOLP_cs 1);


140 
result();


141 


142 
writeln"Problems requiring quantifier duplication";


143 


144 
(*Needs multiple instantiation of ALL.*)


145 
(*


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


147 
by (best_tac FOLP_dup_cs 1);


148 
result();


149 
*)


150 
(*Needs double instantiation of the quantifier*)


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


152 
by (best_tac FOLP_dup_cs 1);


153 
result();


154 


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


156 
by (best_tac FOLP_dup_cs 1);


157 
result();


158 


159 


160 
writeln"Hard examples with quantifiers";


161 


162 
writeln"Problem 18";


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


164 
by (best_tac FOLP_dup_cs 1);


165 
result();


166 


167 
writeln"Problem 19";


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


169 
by (best_tac FOLP_dup_cs 1);


170 
result();


171 


172 
writeln"Problem 20";


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


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


175 
by (fast_tac FOLP_cs 1);


176 
result();


177 
(*


178 
writeln"Problem 21";


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


180 
by (best_tac FOLP_dup_cs 1);


181 
result();


182 
*)


183 
writeln"Problem 22";


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


185 
by (fast_tac FOLP_cs 1);


186 
result();


187 


188 
writeln"Problem 23";


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


190 
by (best_tac FOLP_cs 1);


191 
result();


192 


193 
writeln"Problem 24";


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


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


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


197 
by (fast_tac FOLP_cs 1);


198 
result();


199 
(*


200 
writeln"Problem 25";


201 
goal FOLP.thy "?p : (EX x. P(x)) & \


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


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


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


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


206 
by (best_tac FOLP_cs 1);


207 
result();


208 


209 
writeln"Problem 26";

1459

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


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

0

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


213 
by (fast_tac FOLP_cs 1);


214 
result();


215 
*)


216 
writeln"Problem 27";


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


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


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


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


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


222 
by (fast_tac FOLP_cs 1);


223 
result();


224 


225 
writeln"Problem 28. AMENDED";


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


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


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


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


230 
by (fast_tac FOLP_cs 1);


231 
result();


232 


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


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


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


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


237 
by (fast_tac FOLP_cs 1);


238 
result();


239 


240 
writeln"Problem 30";


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


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


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


244 
by (fast_tac FOLP_cs 1);


245 
result();


246 


247 
writeln"Problem 31";


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


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


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


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


252 
by (fast_tac FOLP_cs 1);


253 
result();


254 


255 
writeln"Problem 32";


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


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


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


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


260 
by (best_tac FOLP_cs 1);


261 
result();


262 


263 
writeln"Problem 33";


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


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


266 
by (best_tac FOLP_cs 1);


267 
result();


268 


269 
writeln"Problem 35";


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


271 
by (best_tac FOLP_dup_cs 1);


272 
result();


273 


274 
writeln"Problem 36";


275 
goal FOLP.thy


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


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


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


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


280 
by (fast_tac FOLP_cs 1);


281 
result();


282 


283 
writeln"Problem 37";


284 
goal FOLP.thy "?p : (ALL z. EX w. ALL x. EX y. \


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


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


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


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


289 
by (fast_tac FOLP_cs 1);


290 
result();


291 


292 
writeln"Problem 39";


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


294 
by (fast_tac FOLP_cs 1);


295 
result();


296 


297 
writeln"Problem 40. AMENDED";


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


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


300 
by (fast_tac FOLP_cs 1);


301 
result();


302 


303 
writeln"Problem 41";

1459

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

0

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


306 
by (best_tac FOLP_cs 1);


307 
result();


308 


309 
writeln"Problem 44";

1459

310 
goal FOLP.thy "?p : (ALL x. f(x) > \


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


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

0

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


314 
by (fast_tac FOLP_cs 1);


315 
result();


316 


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


318 


319 
writeln"Problem 48";


320 
goal FOLP.thy "?p : (a=b  c=d) & (a=c  b=d) > a=d  b=c";


321 
by (fast_tac FOLP_cs 1);


322 
result();


323 


324 
writeln"Problem 50";


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


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


327 
by (best_tac FOLP_dup_cs 1);


328 
result();


329 


330 
writeln"Problem 56";


331 
goal FOLP.thy


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


333 
by (fast_tac FOLP_cs 1);


334 
result();


335 


336 
writeln"Problem 57";


337 
goal FOLP.thy


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


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


340 
by (fast_tac FOLP_cs 1);


341 
result();


342 


343 
writeln"Problem 58 NOT PROVED AUTOMATICALLY";


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


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


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


347 
result();


348 


349 
writeln"Problem 59";


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


351 
by (best_tac FOLP_dup_cs 1);


352 
result();


353 


354 
writeln"Problem 60";


355 
goal FOLP.thy


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


357 
by (fast_tac FOLP_cs 1);


358 
result();


359 


360 
writeln"Reached end of file.";
