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 

17481

15 
context (theory "LK");

7119

16 


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


18 
by (Fast_tac 1);

17481

19 
result();

6252

20 

7119

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


22 
by (Fast_tac 1);

17481

23 
result();

6252

24 

7119

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


26 
by (Fast_tac 1);

17481

27 
result();

6252

28 

7119

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


30 
by (Fast_tac 1);

17481

31 
result();

6252

32 


33 
writeln"Problems requiring quantifier duplication";


34 

7119

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


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

6252

37 
by (best_tac LK_dup_pack 1);


38 
result();


39 


40 
(*Needs double instantiation of the quantifier*)

7119

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

6252

42 
by (fast_tac LK_dup_pack 1);


43 
result();


44 

7119

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

6252

46 
by (best_tac LK_dup_pack 1);


47 
result();


48 


49 
writeln"Hard examples with quantifiers";


50 


51 
writeln"Problem 18";

7119

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

6252

53 
by (best_tac LK_dup_pack 1);

17481

54 
result();

6252

55 


56 
writeln"Problem 19";

7119

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

6252

58 
by (best_tac LK_dup_pack 1);


59 
result();


60 


61 
writeln"Problem 20";

7119

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

6252

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

17481

64 
by (Fast_tac 1);

6252

65 
result();


66 


67 
writeln"Problem 21";

7119

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

6252

69 
by (best_tac LK_dup_pack 1);


70 
result();


71 


72 
writeln"Problem 22";

7119

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

17481

74 
by (Fast_tac 1);

6252

75 
result();


76 


77 
writeln"Problem 23";

7119

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

17481

79 
by (best_tac LK_pack 1);

6252

80 
result();


81 


82 
writeln"Problem 24";

7119

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

6252

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";

7119

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

6252

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))";

17481

95 
by (best_tac LK_pack 1);

6252

96 
result();


97 


98 
writeln"Problem 26";

7119

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

6252

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";

7119

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

6252

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))";

17481

111 
by (pc_tac LK_pack 1);

6252

112 
result();


113 


114 
writeln"Problem 28. AMENDED";

7119

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

6252

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))";

17481

119 
by (pc_tac LK_pack 1);

6252

120 
result();


121 


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

7119

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

6252

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)))";

17481

126 
by (pc_tac LK_pack 1);

6252

127 
result();


128 


129 
writeln"Problem 30";

7119

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

6252

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


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

17481

133 
by (Fast_tac 1);

6252

134 
result();


135 


136 
writeln"Problem 31";

7119

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

6252

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


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


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

7119

141 
by (Fast_tac 1);

6252

142 
result();


143 


144 
writeln"Problem 32";

7119

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

6252

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";

7119

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

6252

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

7119

155 
by (Fast_tac 1);

6252

156 
result();


157 

7119

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

6252

159 
(*Andrews's challenge*)

7119

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

6252

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))))";

7119

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

6252

165 
result();


166 


167 


168 
writeln"Problem 35";

7119

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


170 
by (best_tac LK_dup_pack 1);

6252

171 
result();


172 


173 
writeln"Problem 36";

7119

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


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


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


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


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


179 
by (Fast_tac 1);

6252

180 
result();


181 


182 
writeln"Problem 37";

7119

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

6252

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


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


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


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


188 
by (pc_tac LK_pack 1);


189 
result();


190 


191 
writeln"Problem 38";

7119

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


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


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


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


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

6252

197 
by (pc_tac LK_pack 1);


198 
result();


199 


200 
writeln"Problem 39";

7119

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


202 
by (Fast_tac 1);

6252

203 
result();


204 


205 
writeln"Problem 40. AMENDED";

7119

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


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


208 
by (Fast_tac 1);

6252

209 
result();


210 


211 
writeln"Problem 41";

7119

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


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


214 
by (Fast_tac 1);

6252

215 
result();


216 


217 
writeln"Problem 42";

7119

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

6252

219 


220 
writeln"Problem 43 NOT PROVED AUTOMATICALLY";

7119

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

6252

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


223 


224 
writeln"Problem 44";

7119

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


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


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


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


229 
by (Fast_tac 1);

6252

230 
result();


231 


232 
writeln"Problem 45";

7119

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

6252

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


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


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


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


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

17481

239 
by (best_tac LK_pack 1);

6252

240 
result();


241 


242 

7119

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


244 


245 
writeln"Problem 48";


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


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


248 
result();


249 

17481

250 
writeln"Problem 50";

7119

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

6252

252 
by (best_tac LK_dup_pack 1);


253 
result();


254 

7119

255 
writeln"Problem 51";


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


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


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


259 
result();


260 


261 
writeln"Problem 52";


262 
(*Almost the same as 51. *)


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


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


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


266 
result();


267 


268 
writeln"Problem 56";


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


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


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


272 
result();


273 

6252

274 
writeln"Problem 57";

7119

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


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


277 
by (Fast_tac 1);


278 
result();


279 


280 
writeln"Problem 58!";


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


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

6252

283 
result();


284 


285 
writeln"Problem 59";


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


287 
operation of the occurs check*)

17481

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

7119

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

6252

290 
by (best_tac LK_dup_pack 1);


291 
result();


292 


293 
writeln"Problem 60";

7119

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


295 
by (Fast_tac 1);


296 
result();


297 


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


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


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


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


302 
by (Fast_tac 1);

6252

303 
result();


304 


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


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


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

17481

308 
(*18 September 2005: loaded in 1.809 secs*)
