137 |
137 |
138 goal FOL.thy "(ALL x.P(x)) | Q <-> (ALL x. P(x) | Q)"; |
138 goal FOL.thy "(ALL x.P(x)) | Q <-> (ALL x. P(x) | Q)"; |
139 by (fast_tac FOL_cs 1); |
139 by (fast_tac FOL_cs 1); |
140 result(); |
140 result(); |
141 |
141 |
|
142 (*Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux, |
|
143 JAR 10 (265-281), 1993. Proof is trivial!*) |
|
144 goal FOL.thy |
|
145 "~ ((EX x.~P(x)) & ((EX x.P(x)) | (EX x.P(x) & Q(x))) & ~ (EX x.P(x)))"; |
|
146 by (fast_tac FOL_cs 1); |
|
147 result(); |
|
148 |
142 writeln"Problems requiring quantifier duplication"; |
149 writeln"Problems requiring quantifier duplication"; |
143 |
150 |
144 (*Needs multiple instantiation of ALL.*) |
151 (*Needs multiple instantiation of ALL.*) |
145 goal FOL.thy "(ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"; |
152 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); |
153 by (best_tac FOL_dup_cs 1); |
200 writeln"Problem 24"; |
207 writeln"Problem 24"; |
201 goal FOL.thy "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \ |
208 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)) \ |
209 \ ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x)) \ |
203 \ --> (EX x. P(x)&R(x))"; |
210 \ --> (EX x. P(x)&R(x))"; |
204 by (fast_tac FOL_cs 1); |
211 by (fast_tac FOL_cs 1); |
205 (*slow*) |
|
206 result(); |
212 result(); |
207 |
213 |
208 writeln"Problem 25"; |
214 writeln"Problem 25"; |
209 goal FOL.thy "(EX x. P(x)) & \ |
215 goal FOL.thy "(EX x. P(x)) & \ |
210 \ (ALL x. L(x) --> ~ (M(x) & R(x))) & \ |
216 \ (ALL x. L(x) --> ~ (M(x) & R(x))) & \ |
218 writeln"Problem 26"; |
224 writeln"Problem 26"; |
219 goal FOL.thy "((EX x. p(x)) <-> (EX x. q(x))) & \ |
225 goal FOL.thy "((EX x. p(x)) <-> (EX x. q(x))) & \ |
220 \ (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y))) \ |
226 \ (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)))"; |
227 \ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"; |
222 by (fast_tac FOL_cs 1); |
228 by (fast_tac FOL_cs 1); |
223 (*slow*) |
|
224 result(); |
229 result(); |
225 |
230 |
226 writeln"Problem 27"; |
231 writeln"Problem 27"; |
227 goal FOL.thy "(EX x. P(x) & ~Q(x)) & \ |
232 goal FOL.thy "(EX x. P(x) & ~Q(x)) & \ |
228 \ (ALL x. P(x) --> R(x)) & \ |
233 \ (ALL x. P(x) --> R(x)) & \ |
229 \ (ALL x. M(x) & L(x) --> P(x)) & \ |
234 \ (ALL x. M(x) & L(x) --> P(x)) & \ |
230 \ ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) \ |
235 \ ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) \ |
231 \ --> (ALL x. M(x) --> ~L(x))"; |
236 \ --> (ALL x. M(x) --> ~L(x))"; |
232 by (fast_tac FOL_cs 1); |
237 by (fast_tac FOL_cs 1); |
233 (*slow*) |
|
234 result(); |
238 result(); |
235 |
239 |
236 writeln"Problem 28. AMENDED"; |
240 writeln"Problem 28. AMENDED"; |
237 goal FOL.thy "(ALL x. P(x) --> (ALL x. Q(x))) & \ |
241 goal FOL.thy "(ALL x. P(x) --> (ALL x. Q(x))) & \ |
238 \ ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & \ |
242 \ ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & \ |
239 \ ((EX x.S(x)) --> (ALL x. L(x) --> M(x))) \ |
243 \ ((EX x.S(x)) --> (ALL x. L(x) --> M(x))) \ |
240 \ --> (ALL x. P(x) & L(x) --> M(x))"; |
244 \ --> (ALL x. P(x) & L(x) --> M(x))"; |
241 by (fast_tac FOL_cs 1); |
245 by (fast_tac FOL_cs 1); |
242 (*slow*) |
|
243 result(); |
246 result(); |
244 |
247 |
245 writeln"Problem 29. Essentially the same as Principia Mathematica *11.71"; |
248 writeln"Problem 29. Essentially the same as Principia Mathematica *11.71"; |
246 goal FOL.thy "(EX x. P(x)) & (EX y. Q(y)) \ |
249 goal FOL.thy "(EX x. P(x)) & (EX y. Q(y)) \ |
247 \ --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <-> \ |
250 \ --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <-> \ |