0

1 
(* Title: LK/ex/hardquant


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
Hard examples with quantifiers. Can be read to test the LK system.


7 
From F. J. Pelletier,


8 
SeventyFive Problems for Testing Automatic Theorem Provers,


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


10 
Errata, JAR 4 (1988), 236236.


11 


12 
Uses pc_tac rather than fast_tac when the former is significantly faster.


13 
*)


14 


15 
writeln"File LK/ex/hardquant.";


16 


17 
goal LK.thy " (ALL x. P(x) & Q(x)) <> (ALL x. P(x)) & (ALL x. Q(x))";


18 
by (fast_tac LK_pack 1);


19 
result();


20 


21 
goal LK.thy " (EX x. P>Q(x)) <> (P > (EX x.Q(x)))";


22 
by (fast_tac LK_pack 1);


23 
result();


24 


25 
goal LK.thy " (EX x.P(x)>Q) <> (ALL x.P(x)) > Q";


26 
by (fast_tac LK_pack 1);


27 
result();


28 


29 
goal LK.thy " (ALL x.P(x))  Q <> (ALL x. P(x)  Q)";


30 
by (fast_tac LK_pack 1);


31 
result();


32 


33 
writeln"Problems requiring quantifier duplication";


34 


35 
(*Not provable by fast_tac LK_pack: needs multiple instantiation of ALL*)


36 
goal LK.thy " (ALL x. P(x)>P(f(x))) & P(d)>P(f(f(f(d))))";


37 
by (best_tac LK_dup_pack 1);


38 
result();


39 


40 
(*Needs double instantiation of the quantifier*)


41 
goal LK.thy " EX x. P(x) > P(a) & P(b)";


42 
by (fast_tac LK_dup_pack 1);


43 
result();


44 


45 
goal LK.thy " EX z. P(z) > (ALL x. P(x))";


46 
by (best_tac LK_dup_pack 1);


47 
result();


48 


49 
writeln"Hard examples with quantifiers";


50 


51 
writeln"Problem 18";


52 
goal LK.thy " EX y. ALL x. P(y)>P(x)";


53 
by (best_tac LK_dup_pack 1);


54 
result();


55 


56 
writeln"Problem 19";


57 
goal LK.thy " EX x. ALL y z. (P(y)>Q(z)) > (P(x)>Q(x))";


58 
by (best_tac LK_dup_pack 1);


59 
result();


60 


61 
writeln"Problem 20";


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


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


64 
by (fast_tac LK_pack 1);


65 
result();


66 


67 
writeln"Problem 21";


68 
goal LK.thy " (EX x. P>Q(x)) & (EX x. Q(x)>P) > (EX x. P<>Q(x))";


69 
by (best_tac LK_dup_pack 1);


70 
result();


71 


72 
writeln"Problem 22";


73 
goal LK.thy " (ALL x. P <> Q(x)) > (P <> (ALL x. Q(x)))";


74 
by (fast_tac LK_pack 1);


75 
result();


76 


77 
writeln"Problem 23";


78 
goal LK.thy " (ALL x. P  Q(x)) <> (P  (ALL x. Q(x)))";


79 
by (best_tac LK_pack 1);


80 
result();


81 


82 
writeln"Problem 24";


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


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


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


86 
by (pc_tac LK_pack 1);


87 
result();


88 


89 
writeln"Problem 25";


90 
goal LK.thy " (EX x. P(x)) & \


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


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


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


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


95 
by (best_tac LK_pack 1);


96 
result();


97 


98 
writeln"Problem 26";


99 
goal LK.thy " ((EX x. p(x)) <> (EX x. q(x))) & \


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


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


102 
by (pc_tac LK_pack 1);


103 
result();


104 


105 
writeln"Problem 27";


106 
goal LK.thy " (EX x. P(x) & ~Q(x)) & \


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


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


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


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


111 
by (pc_tac LK_pack 1);


112 
result();


113 


114 
writeln"Problem 28. AMENDED";


115 
goal LK.thy " (ALL x. P(x) > (ALL x. Q(x))) & \


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


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


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


119 
by (pc_tac LK_pack 1);


120 
result();


121 


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


123 
goal LK.thy " (EX x. P(x)) & (EX y. Q(y)) \


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


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


126 
by (pc_tac LK_pack 1);


127 
result();


128 


129 
writeln"Problem 30";


130 
goal LK.thy " (ALL x. P(x)  Q(x) > ~ R(x)) & \


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


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


133 
by (fast_tac LK_pack 1);


134 
result();


135 


136 
writeln"Problem 31";


137 
goal LK.thy " ~(EX x.P(x) & (Q(x)  R(x))) & \


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


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


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


141 
by (fast_tac LK_pack 1);


142 
result();


143 


144 
writeln"Problem 32";


145 
goal LK.thy " (ALL x. P(x) & (Q(x)R(x))>S(x)) & \


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


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


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


149 
by (best_tac LK_pack 1);


150 
result();


151 


152 
writeln"Problem 33";


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


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


155 
by (fast_tac LK_pack 1);


156 
result();


157 


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


159 
(*Andrews's challenge*)


160 
goal LK.thy " ((EX x. ALL y. p(x) <> p(y)) <> \


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


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


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


164 
by (safe_goal_tac LK_pack 1); (*53 secs*) (*13 secs*)


165 
by (TRYALL (fast_tac LK_pack)); (*165 secs*) (*117 secs*) (*138 secs*)


166 
(*for some reason, pc_tac leaves 14 subgoals instead of 6*)


167 
by (TRYALL (best_tac LK_dup_pack)); (*55 secs*) (*29 secs*) (*54 secs*)


168 
result();


169 


170 


171 
writeln"Problem 35";


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


173 
by (best_tac LK_dup_pack 1); (*27 secs??*)


174 
result();


175 


176 
writeln"Problem 36";


177 
goal LK.thy " (ALL x. EX y. J(x,y)) & \


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


179 
\ (ALL x y. J(x,y)  G(x,y) > \


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


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


182 
by (fast_tac LK_pack 1);


183 
result();


184 


185 
writeln"Problem 37";


186 
goal LK.thy " (ALL z. EX w. ALL x. EX y. \


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


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


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


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


191 
by (pc_tac LK_pack 1); (*slow*)


192 
by flexflex_tac;


193 
result();


194 


195 
writeln"Problem 38. NOT PROVED";


196 
goal LK.thy


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


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


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


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


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


202 


203 
writeln"Problem 39";


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


205 
by (fast_tac LK_pack 1);


206 
result();


207 


208 
writeln"Problem 40. AMENDED";


209 
goal LK.thy " (EX y. ALL x. F(x,y) <> F(x,x)) > \


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


211 
by (fast_tac LK_pack 1);


212 
result();


213 


214 
writeln"Problem 41";


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


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


217 
by (fast_tac LK_pack 1);


218 
result();


219 


220 
writeln"Problem 42";


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


222 


223 
writeln"Problem 43 NOT PROVED AUTOMATICALLY";


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


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


226 


227 
writeln"Problem 44";


228 
goal LK.thy " (ALL x. f(x) > \


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


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


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


232 
by (fast_tac LK_pack 1);


233 
result();


234 


235 
writeln"Problem 45";


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


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


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


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


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


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


242 
by (best_tac LK_pack 1);


243 
result();


244 


245 


246 
writeln"Problem 50";


247 
goal LK.thy


248 
" (ALL x. P(a,x)  (ALL y.P(x,y))) > (EX x. ALL y.P(x,y))";


249 
by (best_tac LK_dup_pack 1);


250 
result();


251 


252 
writeln"Problem 57";


253 
goal LK.thy


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


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


256 
by (fast_tac LK_pack 1);


257 
result();


258 


259 
writeln"Problem 59";


260 
(*Unification works poorly here  the abstraction %sobj prevents efficient


261 
operation of the occurs check*)


262 
Unify.trace_bound := !Unify.search_bound  1;


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


264 
by (best_tac LK_dup_pack 1);


265 
result();


266 


267 
writeln"Problem 60";


268 
goal LK.thy


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


270 
by (fast_tac LK_pack 1);


271 
result();


272 


273 
writeln"Reached end of file.";


274 


275 
(*18 June 92: loaded in 372 secs*)


276 
(*19 June 92: loaded in 166 secs except #34, using repeat_goal_tac*)


277 
(*29 June 92: loaded in 370 secs*)
