6252

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 

7119

17 
context LK.thy;


18 


19 
Goal " (ALL x. P(x) & Q(x)) <> (ALL x. P(x)) & (ALL x. Q(x))";


20 
by (Fast_tac 1);

6252

21 
result();


22 

7119

23 
Goal " (EX x. P>Q(x)) <> (P > (EX x. Q(x)))";


24 
by (Fast_tac 1);

6252

25 
result();


26 

7119

27 
Goal " (EX x. P(x)>Q) <> (ALL x. P(x)) > Q";


28 
by (Fast_tac 1);

6252

29 
result();


30 

7119

31 
Goal " (ALL x. P(x))  Q <> (ALL x. P(x)  Q)";


32 
by (Fast_tac 1);

6252

33 
result();


34 


35 
writeln"Problems requiring quantifier duplication";


36 

7119

37 
(*Not provable by Fast_tac: needs multiple instantiation of ALL*)


38 
Goal " (ALL x. P(x)>P(f(x))) & P(d)>P(f(f(f(d))))";

6252

39 
by (best_tac LK_dup_pack 1);


40 
result();


41 


42 
(*Needs double instantiation of the quantifier*)

7119

43 
Goal " EX x. P(x) > P(a) & P(b)";

6252

44 
by (fast_tac LK_dup_pack 1);


45 
result();


46 

7119

47 
Goal " EX z. P(z) > (ALL x. P(x))";

6252

48 
by (best_tac LK_dup_pack 1);


49 
result();


50 


51 
writeln"Hard examples with quantifiers";


52 


53 
writeln"Problem 18";

7119

54 
Goal " EX y. ALL x. P(y)>P(x)";

6252

55 
by (best_tac LK_dup_pack 1);


56 
result();


57 


58 
writeln"Problem 19";

7119

59 
Goal " EX x. ALL y z. (P(y)>Q(z)) > (P(x)>Q(x))";

6252

60 
by (best_tac LK_dup_pack 1);


61 
result();


62 


63 
writeln"Problem 20";

7119

64 
Goal " (ALL x y. EX z. ALL w. (P(x)&Q(y)>R(z)&S(w))) \

6252

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

7119

66 
by (Fast_tac 1);

6252

67 
result();


68 


69 
writeln"Problem 21";

7119

70 
Goal " (EX x. P>Q(x)) & (EX x. Q(x)>P) > (EX x. P<>Q(x))";

6252

71 
by (best_tac LK_dup_pack 1);


72 
result();


73 


74 
writeln"Problem 22";

7119

75 
Goal " (ALL x. P <> Q(x)) > (P <> (ALL x. Q(x)))";


76 
by (Fast_tac 1);

6252

77 
result();


78 


79 
writeln"Problem 23";

7119

80 
Goal " (ALL x. P  Q(x)) <> (P  (ALL x. Q(x)))";

6252

81 
by (best_tac LK_pack 1);


82 
result();


83 


84 
writeln"Problem 24";

7119

85 
Goal " ~(EX x. S(x)&Q(x)) & (ALL x. P(x) > Q(x)R(x)) & \

6252

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


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


88 
by (pc_tac LK_pack 1);


89 
result();


90 


91 
writeln"Problem 25";

7119

92 
Goal " (EX x. P(x)) & \

6252

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


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


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


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


97 
by (best_tac LK_pack 1);


98 
result();


99 


100 
writeln"Problem 26";

7119

101 
Goal " ((EX x. p(x)) <> (EX x. q(x))) & \

6252

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


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


104 
by (pc_tac LK_pack 1);


105 
result();


106 


107 
writeln"Problem 27";

7119

108 
Goal " (EX x. P(x) & ~Q(x)) & \

6252

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


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


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


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


113 
by (pc_tac LK_pack 1);


114 
result();


115 


116 
writeln"Problem 28. AMENDED";

7119

117 
Goal " (ALL x. P(x) > (ALL x. Q(x))) & \

6252

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


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


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


121 
by (pc_tac LK_pack 1);


122 
result();


123 


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

7119

125 
Goal " (EX x. P(x)) & (EX y. Q(y)) \

6252

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


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


128 
by (pc_tac LK_pack 1);


129 
result();


130 


131 
writeln"Problem 30";

7119

132 
Goal " (ALL x. P(x)  Q(x) > ~ R(x)) & \

6252

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


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

7119

135 
by (Fast_tac 1);

6252

136 
result();


137 


138 
writeln"Problem 31";

7119

139 
Goal " ~(EX x. P(x) & (Q(x)  R(x))) & \

6252

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


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


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

7119

143 
by (Fast_tac 1);

6252

144 
result();


145 


146 
writeln"Problem 32";

7119

147 
Goal " (ALL x. P(x) & (Q(x)R(x))>S(x)) & \

6252

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


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


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


151 
by (best_tac LK_pack 1);


152 
result();


153 


154 
writeln"Problem 33";

7119

155 
Goal " (ALL x. P(a) & (P(x)>P(b))>P(c)) <> \

6252

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

7119

157 
by (Fast_tac 1);

6252

158 
result();


159 

7119

160 
writeln"Problem 34 AMENDED (TWICE!!)";

6252

161 
(*Andrews's challenge*)

7119

162 
Goal " ((EX x. ALL y. p(x) <> p(y)) <> \

6252

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


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


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

7119

166 
by (best_tac LK_dup_pack 1); (*10 secs!*)

6252

167 
result();


168 


169 


170 
writeln"Problem 35";

7119

171 
Goal " EX x y. P(x,y) > (ALL u v. P(u,v))";


172 
by (best_tac LK_dup_pack 1);

6252

173 
result();


174 


175 
writeln"Problem 36";

7119

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


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


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


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


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


181 
by (Fast_tac 1);

6252

182 
result();


183 


184 
writeln"Problem 37";

7119

185 
Goal " (ALL z. EX w. ALL x. EX y. \

6252

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


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


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


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


190 
by (pc_tac LK_pack 1);


191 
result();


192 


193 
writeln"Problem 38";

7119

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


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


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


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


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

6252

199 
by (pc_tac LK_pack 1);


200 
result();


201 


202 
writeln"Problem 39";

7119

203 
Goal " ~ (EX x. ALL y. F(y,x) <> ~F(y,y))";


204 
by (Fast_tac 1);

6252

205 
result();


206 


207 
writeln"Problem 40. AMENDED";

7119

208 
Goal " (EX y. ALL x. F(x,y) <> F(x,x)) > \


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


210 
by (Fast_tac 1);

6252

211 
result();


212 


213 
writeln"Problem 41";

7119

214 
Goal " (ALL z. EX y. ALL x. f(x,y) <> f(x,z) & ~ f(x,x)) \


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


216 
by (Fast_tac 1);

6252

217 
result();


218 


219 
writeln"Problem 42";

7119

220 
Goal " ~ (EX y. ALL x. p(x,y) <> ~ (EX z. p(x,z) & p(z,x)))";

6252

221 


222 
writeln"Problem 43 NOT PROVED AUTOMATICALLY";

7119

223 
Goal " (ALL x. ALL y. q(x,y) <> (ALL z. p(z,x) <> p(z,y))) \

6252

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


225 


226 
writeln"Problem 44";

7119

227 
Goal " (ALL x. f(x) > \


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


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


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


231 
by (Fast_tac 1);

6252

232 
result();


233 


234 
writeln"Problem 45";

7119

235 
Goal " (ALL x. f(x) & (ALL y. g(y) & h(x,y) > j(x,y)) \

6252

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


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


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


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


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


241 
by (best_tac LK_pack 1);


242 
result();


243 


244 

7119

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


246 


247 
writeln"Problem 48";


248 
Goal " (a=b  c=d) & (a=c  b=d) > a=d  b=c";


249 
by (fast_tac (pack() add_safes [subst]) 1);


250 
result();


251 

6252

252 
writeln"Problem 50";

7119

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

6252

254 
by (best_tac LK_dup_pack 1);


255 
result();


256 

7119

257 
writeln"Problem 51";


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


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


260 
by (fast_tac (pack() add_safes [subst]) 1);


261 
result();


262 


263 
writeln"Problem 52";


264 
(*Almost the same as 51. *)


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


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


267 
by (fast_tac (pack() add_safes [subst]) 1);


268 
result();


269 


270 
writeln"Problem 56";


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


272 
by (best_tac (pack() add_unsafes [symL, subst]) 1);


273 
(*requires tricker to orient the equality properly*)


274 
result();


275 

6252

276 
writeln"Problem 57";

7119

277 
Goal " P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \


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


279 
by (Fast_tac 1);


280 
result();


281 


282 
writeln"Problem 58!";


283 
Goal " (ALL x y. f(x)=g(y)) > (ALL x y. f(f(x))=f(g(y)))";


284 
by (fast_tac (pack() add_safes [subst]) 1);

6252

285 
result();


286 


287 
writeln"Problem 59";


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


289 
operation of the occurs check*)


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

7119

291 
Goal " (ALL x. P(x) <> ~P(f(x))) > (EX x. P(x) & ~P(f(x)))";

6252

292 
by (best_tac LK_dup_pack 1);


293 
result();


294 


295 
writeln"Problem 60";

7119

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


297 
by (Fast_tac 1);


298 
result();


299 


300 
writeln"Problem 62 as corrected in JAR 18 (1997), page 135";


301 
Goal " (ALL x. p(a) & (p(x) > p(f(x))) > p(f(f(x)))) <> \


302 
\ (ALL x. (~p(a)  p(x)  p(f(f(x)))) & \


303 
\ (~p(a)  ~p(f(x))  p(f(f(x)))))";


304 
by (Fast_tac 1);

6252

305 
result();


306 


307 
writeln"Reached end of file.";


308 


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


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


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