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 


142 
writeln"Problems requiring quantifier duplication";


143 


144 
(*Needs multiple instantiation of ALL.*)


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


146 
by (best_tac FOL_dup_cs 1);


147 
result();


148 


149 
(*Needs double instantiation of the quantifier*)


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


151 
by (best_tac FOL_dup_cs 1);


152 
result();


153 


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


155 
by (best_tac FOL_dup_cs 1);


156 
result();


157 


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


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


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


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


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


163 


164 
writeln"Hard examples with quantifiers";


165 


166 
writeln"Problem 18";


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


168 
by (best_tac FOL_dup_cs 1);


169 
result();


170 


171 
writeln"Problem 19";


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


173 
by (best_tac FOL_dup_cs 1);


174 
result();


175 


176 
writeln"Problem 20";


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


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


179 
by (fast_tac FOL_cs 1);


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


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


182 
by (fast_tac FOL_cs 1);


183 
result();


184 


185 
writeln"Problem 21";


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


187 
by (best_tac FOL_dup_cs 1);


188 
result();


189 


190 
writeln"Problem 22";


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


192 
by (fast_tac FOL_cs 1);


193 
result();


194 


195 
writeln"Problem 23";


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


197 
by (best_tac FOL_cs 1);


198 
result();


199 


200 
writeln"Problem 24";


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


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


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


204 
by (fast_tac FOL_cs 1);


205 
(*slow*)


206 
result();


207 


208 
writeln"Problem 25";


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


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


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


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


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


214 
by (best_tac FOL_cs 1);


215 
(*slow*)


216 
result();


217 


218 
writeln"Problem 26";


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


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


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


222 
by (fast_tac FOL_cs 1);


223 
(*slow*)


224 
result();


225 


226 
writeln"Problem 27";


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


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


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


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


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


232 
by (fast_tac FOL_cs 1);


233 
(*slow*)


234 
result();


235 


236 
writeln"Problem 28. AMENDED";


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


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


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


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


241 
by (fast_tac FOL_cs 1);


242 
(*slow*)


243 
result();


244 


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


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


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


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


249 
by (fast_tac FOL_cs 1);


250 
result();


251 


252 
writeln"Problem 30";


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


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


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


256 
by (fast_tac FOL_cs 1);


257 
result();


258 


259 
writeln"Problem 31";


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


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


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


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


264 
by (fast_tac FOL_cs 1);


265 
result();


266 


267 
writeln"Problem 32";


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


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


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


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


272 
by (best_tac FOL_cs 1);


273 
result();


274 


275 
writeln"Problem 33";


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


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


278 
by (best_tac FOL_cs 1);


279 
result();


280 


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


282 
(*Andrews's challenge*)


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


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


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


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


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


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


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


290 
result();


291 


292 
writeln"Problem 35";


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


294 
by (best_tac FOL_dup_cs 1);


295 
(*6.1 secs*)


296 
result();


297 


298 
writeln"Problem 36";


299 
goal FOL.thy


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


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


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


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


304 
by (fast_tac FOL_cs 1);


305 
result();


306 


307 
writeln"Problem 37";


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


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


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


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


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


313 
by (fast_tac FOL_cs 1);


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


315 
result();


316 


317 
writeln"Problem 38. NOT PROVED";


318 
goal FOL.thy


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


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


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


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


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


324 


325 
writeln"Problem 39";


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


327 
by (fast_tac FOL_cs 1);


328 
result();


329 


330 
writeln"Problem 40. AMENDED";


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


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


333 
by (fast_tac FOL_cs 1);


334 
result();


335 


336 
writeln"Problem 41";


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


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


339 
by (best_tac FOL_cs 1);


340 
result();


341 


342 
writeln"Problem 42 NOT PROVED";


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


344 


345 
writeln"Problem 43 NOT PROVED AUTOMATICALLY";


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


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


348 


349 


350 
writeln"Problem 44";


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


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


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


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


355 
by (fast_tac FOL_cs 1);


356 
result();


357 


358 
writeln"Problem 45";


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


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


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


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


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


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


365 
by (best_tac FOL_cs 1);


366 
(*41.5 secs*)


367 
result();


368 


369 


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


371 


372 
writeln"Problem 48";


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


374 
by (fast_tac FOL_cs 1);


375 
result();


376 


377 
writeln"Problem 49 NOT PROVED AUTOMATICALLY";


378 
(*Hard because it involves substitution for Vars;


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


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


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


382 
by (safe_tac FOL_cs);


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


384 
ba 1;


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


386 
ba 1;


387 
by (fast_tac FOL_cs 1);


388 
result();


389 


390 
writeln"Problem 50";


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


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


393 
by (best_tac FOL_dup_cs 1);


394 
result();


395 


396 
writeln"Problem 51";


397 
goal FOL.thy


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


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


400 
by (fast_tac FOL_cs 1);


401 
result();


402 


403 
writeln"Problem 52";


404 
(*Almost the same as 51. *)


405 
goal FOL.thy


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


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


408 
by (best_tac FOL_cs 1);


409 
result();


410 


411 
writeln"Problem 55";


412 


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


414 
goal FOL.thy


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


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


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


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


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


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


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


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


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


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


425 
\ ~ agatha=butler > \


426 
\ killed(?who,agatha)";


427 
by (safe_tac FOL_cs);


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


429 
ba 1;


430 
be (spec RS exE) 1;


431 
by (REPEAT (etac allE 1));


432 
by (fast_tac FOL_cs 1);


433 
result();


434 
****)


435 


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


437 
fast_tac DISCOVERS who killed Agatha. *)


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


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


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


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


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


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


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


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


446 
\ killed(?who,agatha)";


447 
by (fast_tac FOL_cs 1);


448 
result();


449 


450 


451 
writeln"Problem 56";


452 
goal FOL.thy


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


454 
by (fast_tac FOL_cs 1);


455 
result();


456 


457 
writeln"Problem 57";


458 
goal FOL.thy


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


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


461 
by (fast_tac FOL_cs 1);


462 
result();


463 


464 
writeln"Problem 58 NOT PROVED AUTOMATICALLY";


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


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


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


468 
result();


469 


470 
writeln"Problem 59";


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


472 
by (best_tac FOL_dup_cs 1);


473 
result();


474 


475 
writeln"Problem 60";


476 
goal FOL.thy


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


478 
by (fast_tac FOL_cs 1);


479 
result();


480 


481 


482 
writeln"Reached end of file.";


483 


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