26322

1 
(* Title: FOLP/ex/Classical.thy


2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


3 
Copyright 1993 University of Cambridge


4 


5 
Classical FirstOrder Logic.


6 
*)


7 


8 
theory Classical


9 
imports FOLP


10 
begin


11 

61337

12 
schematic_goal "?p : (P > Q  R) > (P>Q)  (P>R)"

58957

13 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

14 


15 
(*If and only if*)

61337

16 
schematic_goal "?p : (P<>Q) <> (Q<>P)"

58957

17 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

18 

61337

19 
schematic_goal "?p : ~ (P <> ~P)"

58957

20 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

21 


22 


23 
(*Sample problems from


24 
F. J. Pelletier,


25 
SeventyFive Problems for Testing Automatic Theorem Provers,


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


27 
Errata, JAR 4 (1988), 236236.


28 


29 
The hardest problems  judging by experience with several theorem provers,


30 
including matrix ones  are 34 and 43.


31 
*)


32 


33 
text "Pelletier's examples"


34 
(*1*)

61337

35 
schematic_goal "?p : (P>Q) <> (~Q > ~P)"

58957

36 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

37 


38 
(*2*)

61337

39 
schematic_goal "?p : ~ ~ P <> P"

58957

40 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

41 


42 
(*3*)

61337

43 
schematic_goal "?p : ~(P>Q) > (Q>P)"

58957

44 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

45 


46 
(*4*)

61337

47 
schematic_goal "?p : (~P>Q) <> (~Q > P)"

58957

48 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

49 


50 
(*5*)

61337

51 
schematic_goal "?p : ((PQ)>(PR)) > (P(Q>R))"

58957

52 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

53 


54 
(*6*)

61337

55 
schematic_goal "?p : P  ~ P"

58957

56 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

57 


58 
(*7*)

61337

59 
schematic_goal "?p : P  ~ ~ ~ P"

58957

60 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

61 


62 
(*8. Peirce's law*)

61337

63 
schematic_goal "?p : ((P>Q) > P) > P"

58957

64 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

65 


66 
(*9*)

61337

67 
schematic_goal "?p : ((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)"

58957

68 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

69 


70 
(*10*)

61337

71 
schematic_goal "?p : (Q>R) & (R>P&Q) & (P>QR) > (P<>Q)"

58957

72 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

73 


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

61337

75 
schematic_goal "?p : P<>P"

58957

76 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

77 


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

61337

79 
schematic_goal "?p : ((P <> Q) <> R) <> (P <> (Q <> R))"

58957

80 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

81 


82 
(*13. Distributive law*)

61337

83 
schematic_goal "?p : P  (Q & R) <> (P  Q) & (P  R)"

58957

84 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

85 


86 
(*14*)

61337

87 
schematic_goal "?p : (P <> Q) <> ((Q  ~P) & (~QP))"

58957

88 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

89 


90 
(*15*)

61337

91 
schematic_goal "?p : (P > Q) <> (~P  Q)"

58957

92 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

93 


94 
(*16*)

61337

95 
schematic_goal "?p : (P>Q)  (Q>P)"

58957

96 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

97 


98 
(*17*)

61337

99 
schematic_goal "?p : ((P & (Q>R))>S) <> ((~P  Q  S) & (~P  ~R  S))"

58957

100 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

101 


102 


103 
text "Classical Logic: examples with quantifiers"


104 

61337

105 
schematic_goal "?p : (ALL x. P(x) & Q(x)) <> (ALL x. P(x)) & (ALL x. Q(x))"

58957

106 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

107 

61337

108 
schematic_goal "?p : (EX x. P>Q(x)) <> (P > (EX x. Q(x)))"

58957

109 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

110 

61337

111 
schematic_goal "?p : (EX x. P(x)>Q) <> (ALL x. P(x)) > Q"

58957

112 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

113 

61337

114 
schematic_goal "?p : (ALL x. P(x))  Q <> (ALL x. P(x)  Q)"

58957

115 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

116 


117 


118 
text "Problems requiring quantifier duplication"


119 


120 
(*Needs multiple instantiation of ALL.*)

61337

121 
schematic_goal "?p : (ALL x. P(x)>P(f(x))) & P(d)>P(f(f(f(d))))"

58957

122 
by (tactic "best_tac @{context} FOLP_dup_cs 1")

26322

123 


124 
(*Needs double instantiation of the quantifier*)

61337

125 
schematic_goal "?p : EX x. P(x) > P(a) & P(b)"

58957

126 
by (tactic "best_tac @{context} FOLP_dup_cs 1")

26322

127 

61337

128 
schematic_goal "?p : EX z. P(z) > (ALL x. P(x))"

58957

129 
by (tactic "best_tac @{context} FOLP_dup_cs 1")

26322

130 


131 


132 
text "Hard examples with quantifiers"


133 


134 
text "Problem 18"

61337

135 
schematic_goal "?p : EX y. ALL x. P(y)>P(x)"

58957

136 
by (tactic "best_tac @{context} FOLP_dup_cs 1")

26322

137 


138 
text "Problem 19"

61337

139 
schematic_goal "?p : EX x. ALL y z. (P(y)>Q(z)) > (P(x)>Q(x))"

58957

140 
by (tactic "best_tac @{context} FOLP_dup_cs 1")

26322

141 


142 
text "Problem 20"

61337

143 
schematic_goal "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)>R(z)&S(w)))

26322

144 
> (EX x y. P(x) & Q(y)) > (EX z. R(z))"

58957

145 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

146 


147 
text "Problem 21"

61337

148 
schematic_goal "?p : (EX x. P>Q(x)) & (EX x. Q(x)>P) > (EX x. P<>Q(x))"

58957

149 
by (tactic "best_tac @{context} FOLP_dup_cs 1")

26322

150 


151 
text "Problem 22"

61337

152 
schematic_goal "?p : (ALL x. P <> Q(x)) > (P <> (ALL x. Q(x)))"

58957

153 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

154 


155 
text "Problem 23"

61337

156 
schematic_goal "?p : (ALL x. P  Q(x)) <> (P  (ALL x. Q(x)))"

58957

157 
by (tactic "best_tac @{context} FOLP_dup_cs 1")

26322

158 


159 
text "Problem 24"

61337

160 
schematic_goal "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) > Q(x)R(x)) &

26322

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


162 
> (EX x. P(x)&R(x))"

58957

163 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

164 


165 
text "Problem 25"

61337

166 
schematic_goal "?p : (EX x. P(x)) &

26322

167 
(ALL x. L(x) > ~ (M(x) & R(x))) &


168 
(ALL x. P(x) > (M(x) & L(x))) &


169 
((ALL x. P(x)>Q(x))  (EX x. P(x)&R(x)))


170 
> (EX x. Q(x)&P(x))"


171 
oops


172 


173 
text "Problem 26"

61337

174 
schematic_goal "?u : ((EX x. p(x)) <> (EX x. q(x))) &

26322

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

58860

176 
> ((ALL x. p(x)>r(x)) <> (ALL x. q(x)>s(x)))"

58957

177 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

178 


179 
text "Problem 27"

61337

180 
schematic_goal "?p : (EX x. P(x) & ~Q(x)) &

26322

181 
(ALL x. P(x) > R(x)) &


182 
(ALL x. M(x) & L(x) > P(x)) &


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


184 
> (ALL x. M(x) > ~L(x))"

58957

185 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

186 


187 
text "Problem 28. AMENDED"

61337

188 
schematic_goal "?p : (ALL x. P(x) > (ALL x. Q(x))) &

26322

189 
((ALL x. Q(x)R(x)) > (EX x. Q(x)&S(x))) &


190 
((EX x. S(x)) > (ALL x. L(x) > M(x)))


191 
> (ALL x. P(x) & L(x) > M(x))"

58957

192 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

193 


194 
text "Problem 29. Essentially the same as Principia Mathematica *11.71"

61337

195 
schematic_goal "?p : (EX x. P(x)) & (EX y. Q(y))

26322

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


197 
(ALL x y. P(x) & Q(y) > R(x) & S(y)))"

58957

198 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

199 


200 
text "Problem 30"

61337

201 
schematic_goal "?p : (ALL x. P(x)  Q(x) > ~ R(x)) &

26322

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


203 
> (ALL x. S(x))"

58957

204 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

205 


206 
text "Problem 31"

61337

207 
schematic_goal "?p : ~(EX x. P(x) & (Q(x)  R(x))) &

26322

208 
(EX x. L(x) & P(x)) &


209 
(ALL x. ~ R(x) > M(x))


210 
> (EX x. L(x) & M(x))"

58957

211 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

212 


213 
text "Problem 32"

61337

214 
schematic_goal "?p : (ALL x. P(x) & (Q(x)R(x))>S(x)) &

26322

215 
(ALL x. S(x) & R(x) > L(x)) &


216 
(ALL x. M(x) > R(x))


217 
> (ALL x. P(x) & M(x) > L(x))"

58957

218 
by (tactic "best_tac @{context} FOLP_dup_cs 1")

26322

219 


220 
text "Problem 33"

61337

221 
schematic_goal "?p : (ALL x. P(a) & (P(x)>P(b))>P(c)) <>

26322

222 
(ALL x. (~P(a)  P(x)  P(c)) & (~P(a)  ~P(b)  P(c)))"

58957

223 
by (tactic "best_tac @{context} FOLP_dup_cs 1")

26322

224 


225 
text "Problem 35"

61337

226 
schematic_goal "?p : EX x y. P(x,y) > (ALL u v. P(u,v))"

58957

227 
by (tactic "best_tac @{context} FOLP_dup_cs 1")

26322

228 


229 
text "Problem 36"

61337

230 
schematic_goal

26322

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


232 
(ALL x. EX y. G(x,y)) &


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


234 
> (ALL x. EX y. H(x,y))"

58957

235 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

236 


237 
text "Problem 37"

61337

238 
schematic_goal "?p : (ALL z. EX w. ALL x. EX y.

26322

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


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


241 
((EX x y. Q(x,y)) > (ALL x. R(x,x)))


242 
> (ALL x. EX y. R(x,y))"

58957

243 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

244 


245 
text "Problem 39"

61337

246 
schematic_goal "?p : ~ (EX x. ALL y. F(y,x) <> ~F(y,y))"

58957

247 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

248 


249 
text "Problem 40. AMENDED"

61337

250 
schematic_goal "?p : (EX y. ALL x. F(x,y) <> F(x,x)) >

26322

251 
~(ALL x. EX y. ALL z. F(z,y) <> ~ F(z,x))"

58957

252 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

253 


254 
text "Problem 41"

61337

255 
schematic_goal "?p : (ALL z. EX y. ALL x. f(x,y) <> f(x,z) & ~ f(x,x))

26322

256 
> ~ (EX z. ALL x. f(x,z))"

58957

257 
by (tactic "best_tac @{context} FOLP_dup_cs 1")

26322

258 


259 
text "Problem 44"

61337

260 
schematic_goal "?p : (ALL x. f(x) >

26322

261 
(EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) &


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


263 
> (EX x. j(x) & ~f(x))"

58957

264 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

265 


266 
text "Problems (mainly) involving equality or functions"


267 


268 
text "Problem 48"

61337

269 
schematic_goal "?p : (a=b  c=d) & (a=c  b=d) > a=d  b=c"

58957

270 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

271 


272 
text "Problem 50"


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

61337

274 
schematic_goal "?p : (ALL x. P(a,x)  (ALL y. P(x,y))) > (EX x. ALL y. P(x,y))"

58957

275 
by (tactic "best_tac @{context} FOLP_dup_cs 1")

26322

276 


277 
text "Problem 56"

61337

278 
schematic_goal

26322

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

58957

280 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

281 


282 
text "Problem 57"

61337

283 
schematic_goal

26322

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


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

58957

286 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

287 


288 
text "Problem 58 NOT PROVED AUTOMATICALLY"

61337

289 
schematic_goal "?p : (ALL x y. f(x)=g(y)) > (ALL x y. f(f(x))=f(g(y)))"

60375

290 
supply f_cong = subst_context [where t = f]

60770

291 
by (tactic \<open>fast_tac @{context} (FOLP_cs addSIs [@{thm f_cong}]) 1\<close>)

26322

292 


293 
text "Problem 59"

61337

294 
schematic_goal "?p : (ALL x. P(x) <> ~P(f(x))) > (EX x. P(x) & ~P(f(x)))"

58957

295 
by (tactic "best_tac @{context} FOLP_dup_cs 1")

26322

296 


297 
text "Problem 60"

61337

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

58957

299 
by (tactic "fast_tac @{context} FOLP_cs 1")

26322

300 


301 
end
