(**** Test Data for Chapter 10 of ML for the Working Programmer, 2nd edition by Lawrence C. Paulson, Computer Laboratory, University of Cambridge. (Cambridge University Press, 1996) Copyright (C) 1996 by Cambridge University Press.Permission to copy without fee is granted provided that this copyrightnotice and the DISCLAIMER OF WARRANTY are included in any copy. DISCLAIMER OF WARRANTY. These programs are provided `as is' withoutwarranty of any kind. We make no warranties, express or implied, that theprograms are free of error, or are consistent with any particular standardof merchantability, or that they will meet your requirements for anyparticular application. They should not be relied upon for solving aproblem whose incorrect solution could result in injury to a person or lossof property. If you do use the programs or functions in such a manner, itis at your own risk. The author and publisher disclaim all liability fordirect, incidental or consequential damages resulting from your use ofthese programs or functions.****) open Command;open Tactical; fun showResult () = if Rule.final(getState()) then DisplayFol.form(Rule.main (getState())) else raise Fail "Unsolved subgoals exist!"; fun checkFailed() = if Rule.final(getState()) then raise Fail "Should have failed!" else "Failed, as expected..."; (*** Single step proofs and basic use of tacticals ***) (*single steps -- essentially the proof * of section 10.2 *)goal "P & Q --> Q & P";by (Rule.impR 1);by (Rule.conjL 1);by (Rule.conjR 1);by (Rule.basic 2);by (Rule.basic 1);showResult(); (* essentially the first quantifier proof, section 10.4 *)goal "(ALL x.P(x)) --> (ALL x. P(x) | Q(x))";by (Rule.impR 1);by (Rule.allR 1);by (Rule.disjR 1);by (Rule.allL 1);by (Rule.unify 1);showResult(); (* the second quantifier proof, section 10.4 *)goal "EX z. P(z) --> (ALL x. P(x))";by (Rule.exR 1);by (Rule.impR 1);by (Rule.allR 1);by (Rule.unify 1); (*FAILS!*)by (Rule.exR 1);by (Rule.impR 1);by (Rule.unify 1);showResult(); goal "(P & Q) & R --> P & (Q & R)";by (Rule.impR 1);by (Rule.conjL 1);by (Rule.conjL 1);by (Rule.conjR 1);by (Rule.conjR 2);by (Rule.basic 1);by (Rule.basic 1);by (Rule.basic 1);showResult(); (** Demonstrating tacticals **) goal "(P & Q) & R --> P & (Q & R)";by (repeat (Rule.impR 1 || Rule.conjL 1));by (repeat (Rule.basic 1 || Rule.conjR 1));showResult(); goal "EX z. P(z) --> (ALL x. P(x))";by (repeat (Rule.unify 1 || Rule.impR 1 || Rule.allR 1 || Rule.exR 1));showResult(); (*single steps*)goal "(P & Q) | R --> (P | R) & (Q | R)";by (Rule.impR 1);by (Rule.disjL 1);by (Rule.conjL 1);by (Rule.conjR 1);by (Rule.disjR 1);by (Rule.disjR 2);by (Rule.conjR 3);by (Rule.disjR 3);by (Rule.disjR 4);by (Rule.basic 1);by (Rule.basic 1);by (Rule.basic 1);by (Rule.basic 1);showResult(); (*single steps*)goal "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";by (Rule.iffR 1);by (Rule.conjR 1);by (Rule.allR 1);by (Rule.allL 1);by (Rule.conjL 1);by (Rule.unify 1);by (Rule.allR 1);by (Rule.allL 1);by (Rule.conjL 1);by (Rule.unify 1);by (Rule.allR 1);by (Rule.conjL 1);by (Rule.allL 1);by (Rule.allL 1);by (Rule.conjR 1);by (Rule.unify 1);by (Rule.unify 1);showResult(); goal "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";by (repeat (Rule.unify 1 || Rule.iffR 1 || Rule.allR 1 || Rule.conjR 1 || Rule.conjL 1 || Rule.allL 1));showResult(); (*single steps -- BASIC TEST OF QUANTIFIER REASONING *)goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";by (Rule.impR 1);by (Rule.exL 1);by (Rule.allR 1);by (Rule.allL 1);by (Rule.exR 1);by (Rule.unify 1);showResult(); (*single steps -- BASIC TEST OF QUANTIFIER REASONING -- INVALID *)goal "(ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))";by (Rule.impR 1);by (Rule.allL 1);by (Rule.exL 1);by (Rule.exR 1);by (Rule.allR 1);by (Rule.unify 1);checkFailed();(*NB. The failure of this proof does not demonstrate that no proof exists!*) goal "(EX x.P(x)-->Q) <-> (ALL x.P(x)) --> Q";by (Rule.iffR 1);by (Rule.impR 1);by (Rule.exL 1);by (Rule.allL 1);by (Rule.impL 1);by (Rule.unify 1);by (Rule.unify 1);by (Rule.impL 1);by (Rule.exR 1);by (Rule.impR 1);by (Rule.unify 1);by (Rule.allR 1);by (Rule.exR 1);by (Rule.impR 1);by (Rule.unify 1);showResult(); (*** Automatic proofs ***) print"commutative laws of & and | \n";goal "P & Q --> Q & P";by Tac.depth;showResult(); goal "P | Q --> Q | P";by Tac.depth;showResult(); print"associative laws of & and | \n";goal "(P & Q) & R --> P & (Q & R)";by Tac.depth;showResult(); goal "(P | Q) | R --> P | (Q | R)";by Tac.depth;showResult(); print"distributive laws of & and | \n";goal "(P & Q) | R --> (P | R) & (Q | R)";by Tac.depth;showResult(); goal "(P | R) & (Q | R) --> (P & Q) | R";by Tac.depth;showResult(); goal "(P | Q) & R --> (P & R) | (Q & R)";by Tac.depth;showResult(); goal "(P & R) | (Q & R) --> (P | Q) & R";by Tac.depth;showResult(); print"Laws involving implication\n"; goal "(P-->R) & (Q-->R) <-> (P|Q --> R)";by Tac.depth;showResult(); goal "(P & Q --> R) <-> (P--> (Q-->R))";by Tac.depth;showResult(); goal "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R";by Tac.depth;showResult(); goal "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)";by Tac.depth;showResult(); goal "(P --> Q & R) <-> (P-->Q) & (P-->R)";by Tac.depth;showResult(); print"Propositions-as-types\n"; (*The combinator K*)goal "P --> (Q --> P)";by Tac.depth;showResult(); (*The combinator S*)goal "(P-->Q-->R) --> (P-->Q) --> (P-->R)";by Tac.depth;showResult(); (*Converse is classical*)goal "(P-->Q) | (P-->R) --> (P --> Q | R)";by Tac.depth;showResult(); goal "(P-->Q) --> (~Q --> ~P)";by Tac.depth;showResult(); print"Classical examples\n"; goal "(P --> Q | R) --> (P-->Q) | (P-->R)";by Tac.depth;showResult(); (*If and only if*) goal "(P<->Q) <-> (Q<->P)";by Tac.depth;showResult(); goal "~ (P <-> ~P)";by Tac.depth;showResult(); print"*** Quantifier examples ***\n"; goal "(ALL x. ALL y.P(x,y)) --> (ALL y. ALL x.P(x,y))";by Tac.depth;showResult(); goal "(EX x. EX y.P(x,y)) --> (EX y. EX x.P(x,y))";by Tac.depth;showResult(); (*Converse is false*)goal "(ALL x.P(x)) | (ALL x.Q(x)) --> (ALL x. P(x) | Q(x))";by Tac.depth;showResult(); goal "(ALL x. P-->Q(x)) <-> (P--> (ALL x.Q(x)))";by Tac.depth;showResult(); goal "(ALL x.P(x)-->Q) <-> ((EX x.P(x)) --> Q)";by Tac.depth;showResult(); print"Some harder ones\n"; goal "(EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))";by Tac.depth;showResult(); (*Converse is false*)goal "(EX x. P(x)&Q(x)) --> (EX x.P(x)) & (EX x.Q(x))";by Tac.depth;showResult(); print"Basic test of quantifier reasoning\n";(*TRUE*)goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";by Tac.depth; showResult(); goal "(ALL x. Q(x)) --> (EX x. Q(x))";by Tac.depth; showResult(); print"The following should fail, as they are false!\n"; goal "(EX x. Q(x)) --> (ALL x. Q(x))";by Tac.depth;checkFailed(); goal "P(?a) --> (ALL x.P(x))";by Tac.depth;checkFailed(); goal "(P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))";by Tac.depth;checkFailed(); print"Back to things that are provable...\n"; goal "(ALL x.P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))";by Tac.depth; showResult(); (*An example of why exists_intr should be delayed as long as possible*)goal "(P --> (EX x.Q(x))) & P --> (EX x.Q(x))";by Tac.depth; showResult(); (*instantiation of the variable ?a *)goal "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";by Tac.depth; showResult(); goal "(ALL x. Q(x)) --> (EX x. Q(x))";by Tac.depth;showResult(); print"Classical Logic: examples with quantifiers.\n"; goal "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";by Tac.depth;showResult(); goal "(EX x. P-->Q(x)) <-> (P --> (EX x.Q(x)))";by Tac.depth;showResult(); goal "(EX x.P(x)-->Q) <-> (ALL x.P(x)) --> Q";by Tac.depth;showResult(); goal "(ALL x.P(x)) | Q <-> (ALL x. P(x) | Q)";by Tac.depth;showResult(); print"Harder proofs \n"; (*This Prolog program needs multiple instantiation of ALL. *)goal "(ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))";by Tac.depth;(***orby (repeat (Tac.safeStep 1 || unify 1 || Rule.allL 1));***)showResult(); (*Needs double instantiation of EXISTS*)goal "EX x. P(x) --> P(a) & P(b)";by Tac.depth;showResult(); goal "EX z. P(z) --> (ALL x. P(x))";by Tac.depth;showResult(); print"Some slow ones\n"; (*Principia Mathematica *11.53 *)goal "(ALL x. ALL y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";by Tac.depth;showResult(); (*Principia Mathematica *11.55 *)goal "(EX x. EX y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";by Tac.depth;showResult(); (*Principia Mathematica *11.61 *)goal "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";by Tac.depth;showResult(); (*Principia Mathematica *11.71 SLOW*)goal "(EX z. P(z)) & (EX w. Q(w)) --> \\ ((ALL z. P(z) --> R(z)) & (ALL w. Q(w) --> S(w)) \\ <-> (ALL z. ALL w. P(z) & Q(w) --> R(z) & S(w)))";by Tac.depth;showResult(); (*from Vladimir Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23*)goal "EX x. EX X. ALL y. EX z. EX Z. \\ (~P(y,y) | P(x,x) | ~S(z,x)) & \\ (S(x,y) | ~S(y,z) | Q(Z,Z)) & \\ (Q(X,y) | ~Q(y,Z) | S(X,X))"; (*Sample problems from F. J. Pelletier, Seventy-Five Problems for Testing Automatic Theorem Provers, J. Automated Reasoning 2 (1986), 191-216. Errata, JAR 4 (1988), 236-236.*) print"Pelletier's examples\n";(*1*)goal "(P-->Q) <-> (~Q --> ~P)";by Tac.depth;showResult(); (*2*)goal "~ ~ P <-> P";by Tac.depth;showResult(); (*3*)goal "~(P-->Q) --> (Q-->P)";by Tac.depth;showResult(); (*4*)goal "(~P-->Q) <-> (~Q --> P)";by Tac.depth;showResult(); (*5*)goal "((P|Q)-->(P|R)) --> (P|(Q-->R))";by Tac.depth;showResult(); (*6*)goal "P | ~ P";by Tac.depth;showResult(); (*7*)goal "P | ~ ~ ~ P";by Tac.depth;showResult(); (*8. Peirce's law*)goal "((P-->Q) --> P) --> P";by Tac.depth;showResult(); (*9*)goal "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";by Tac.depth;showResult(); (*10*)goal "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)";by Tac.depth;showResult(); (*11. Proved in each direction (incorrectly, says Pelletier!!) *)Lines 1–500 of 793. Load more
(**** Test Data for Chapter 10 of ML for the Working Programmer, 2nd edition by Lawrence C. Paulson, Computer Laboratory, University of Cambridge. (Cambridge University Press, 1996) Copyright (C) 1996 by Cambridge University Press. Permission to copy without fee is granted provided that this copyright notice and the DISCLAIMER OF WARRANTY are included in any copy. DISCLAIMER OF WARRANTY. These programs are provided `as is' without warranty of any kind. We make no warranties, express or implied, that the programs are free of error, or are consistent with any particular standard of merchantability, or that they will meet your requirements for any particular application. They should not be relied upon for solving a problem whose incorrect solution could result in injury to a person or loss of property. If you do use the programs or functions in such a manner, it is at your own risk. The author and publisher disclaim all liability for direct, incidental or consequential damages resulting from your use of these programs or functions. ****) open Command; open Tactical; fun showResult () = if Rule.final(getState()) then DisplayFol.form(Rule.main (getState())) else raise Fail "Unsolved subgoals exist!"; fun checkFailed() = if Rule.final(getState()) then raise Fail "Should have failed!" else "Failed, as expected..."; (*** Single step proofs and basic use of tacticals ***) (*single steps -- essentially the proof * of section 10.2 *) goal "P & Q --> Q & P"; by (Rule.impR 1); by (Rule.conjL 1); by (Rule.conjR 1); by (Rule.basic 2); by (Rule.basic 1); showResult(); (* essentially the first quantifier proof, section 10.4 *) goal "(ALL x.P(x)) --> (ALL x. P(x) | Q(x))"; by (Rule.impR 1); by (Rule.allR 1); by (Rule.disjR 1); by (Rule.allL 1); by (Rule.unify 1); showResult(); (* the second quantifier proof, section 10.4 *) goal "EX z. P(z) --> (ALL x. P(x))"; by (Rule.exR 1); by (Rule.impR 1); by (Rule.allR 1); by (Rule.unify 1); (*FAILS!*) by (Rule.exR 1); by (Rule.impR 1); by (Rule.unify 1); showResult(); goal "(P & Q) & R --> P & (Q & R)"; by (Rule.impR 1); by (Rule.conjL 1); by (Rule.conjL 1); by (Rule.conjR 1); by (Rule.conjR 2); by (Rule.basic 1); by (Rule.basic 1); by (Rule.basic 1); showResult(); (** Demonstrating tacticals **) goal "(P & Q) & R --> P & (Q & R)"; by (repeat (Rule.impR 1 || Rule.conjL 1)); by (repeat (Rule.basic 1 || Rule.conjR 1)); showResult(); goal "EX z. P(z) --> (ALL x. P(x))"; by (repeat (Rule.unify 1 || Rule.impR 1 || Rule.allR 1 || Rule.exR 1)); showResult(); (*single steps*) goal "(P & Q) | R --> (P | R) & (Q | R)"; by (Rule.impR 1); by (Rule.disjL 1); by (Rule.conjL 1); by (Rule.conjR 1); by (Rule.disjR 1); by (Rule.disjR 2); by (Rule.conjR 3); by (Rule.disjR 3); by (Rule.disjR 4); by (Rule.basic 1); by (Rule.basic 1); by (Rule.basic 1); by (Rule.basic 1); showResult(); (*single steps*) goal "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"; by (Rule.iffR 1); by (Rule.conjR 1); by (Rule.allR 1); by (Rule.allL 1); by (Rule.conjL 1); by (Rule.unify 1); by (Rule.allR 1); by (Rule.allL 1); by (Rule.conjL 1); by (Rule.unify 1); by (Rule.allR 1); by (Rule.conjL 1); by (Rule.allL 1); by (Rule.allL 1); by (Rule.conjR 1); by (Rule.unify 1); by (Rule.unify 1); showResult(); goal "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"; by (repeat (Rule.unify 1 || Rule.iffR 1 || Rule.allR 1 || Rule.conjR 1 || Rule.conjL 1 || Rule.allL 1)); showResult(); (*single steps -- BASIC TEST OF QUANTIFIER REASONING *) goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; by (Rule.impR 1); by (Rule.exL 1); by (Rule.allR 1); by (Rule.allL 1); by (Rule.exR 1); by (Rule.unify 1); showResult(); (*single steps -- BASIC TEST OF QUANTIFIER REASONING -- INVALID *) goal "(ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"; by (Rule.impR 1); by (Rule.allL 1); by (Rule.exL 1); by (Rule.exR 1); by (Rule.allR 1); by (Rule.unify 1); checkFailed(); (*NB. The failure of this proof does not demonstrate that no proof exists!*) goal "(EX x.P(x)-->Q) <-> (ALL x.P(x)) --> Q"; by (Rule.iffR 1); by (Rule.impR 1); by (Rule.exL 1); by (Rule.allL 1); by (Rule.impL 1); by (Rule.unify 1); by (Rule.unify 1); by (Rule.impL 1); by (Rule.exR 1); by (Rule.impR 1); by (Rule.unify 1); by (Rule.allR 1); by (Rule.exR 1); by (Rule.impR 1); by (Rule.unify 1); showResult(); (*** Automatic proofs ***) print"commutative laws of & and | \n"; goal "P & Q --> Q & P"; by Tac.depth; showResult(); goal "P | Q --> Q | P"; by Tac.depth; showResult(); print"associative laws of & and | \n"; goal "(P & Q) & R --> P & (Q & R)"; by Tac.depth; showResult(); goal "(P | Q) | R --> P | (Q | R)"; by Tac.depth; showResult(); print"distributive laws of & and | \n"; goal "(P & Q) | R --> (P | R) & (Q | R)"; by Tac.depth; showResult(); goal "(P | R) & (Q | R) --> (P & Q) | R"; by Tac.depth; showResult(); goal "(P | Q) & R --> (P & R) | (Q & R)"; by Tac.depth; showResult(); goal "(P & R) | (Q & R) --> (P | Q) & R"; by Tac.depth; showResult(); print"Laws involving implication\n"; goal "(P-->R) & (Q-->R) <-> (P|Q --> R)"; by Tac.depth; showResult(); goal "(P & Q --> R) <-> (P--> (Q-->R))"; by Tac.depth; showResult(); goal "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"; by Tac.depth; showResult(); goal "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"; by Tac.depth; showResult(); goal "(P --> Q & R) <-> (P-->Q) & (P-->R)"; by Tac.depth; showResult(); print"Propositions-as-types\n"; (*The combinator K*) goal "P --> (Q --> P)"; by Tac.depth; showResult(); (*The combinator S*) goal "(P-->Q-->R) --> (P-->Q) --> (P-->R)"; by Tac.depth; showResult(); (*Converse is classical*) goal "(P-->Q) | (P-->R) --> (P --> Q | R)"; by Tac.depth; showResult(); goal "(P-->Q) --> (~Q --> ~P)"; by Tac.depth; showResult(); print"Classical examples\n"; goal "(P --> Q | R) --> (P-->Q) | (P-->R)"; by Tac.depth; showResult(); (*If and only if*) goal "(P<->Q) <-> (Q<->P)"; by Tac.depth; showResult(); goal "~ (P <-> ~P)"; by Tac.depth; showResult(); print"*** Quantifier examples ***\n"; goal "(ALL x. ALL y.P(x,y)) --> (ALL y. ALL x.P(x,y))"; by Tac.depth; showResult(); goal "(EX x. EX y.P(x,y)) --> (EX y. EX x.P(x,y))"; by Tac.depth; showResult(); (*Converse is false*) goal "(ALL x.P(x)) | (ALL x.Q(x)) --> (ALL x. P(x) | Q(x))"; by Tac.depth; showResult(); goal "(ALL x. P-->Q(x)) <-> (P--> (ALL x.Q(x)))"; by Tac.depth; showResult(); goal "(ALL x.P(x)-->Q) <-> ((EX x.P(x)) --> Q)"; by Tac.depth; showResult(); print"Some harder ones\n"; goal "(EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))"; by Tac.depth; showResult(); (*Converse is false*) goal "(EX x. P(x)&Q(x)) --> (EX x.P(x)) & (EX x.Q(x))"; by Tac.depth; showResult(); print"Basic test of quantifier reasoning\n"; (*TRUE*) goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; by Tac.depth; showResult(); goal "(ALL x. Q(x)) --> (EX x. Q(x))"; by Tac.depth; showResult(); print"The following should fail, as they are false!\n"; goal "(EX x. Q(x)) --> (ALL x. Q(x))"; by Tac.depth; checkFailed(); goal "P(?a) --> (ALL x.P(x))"; by Tac.depth; checkFailed(); goal "(P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))"; by Tac.depth; checkFailed(); print"Back to things that are provable...\n"; goal "(ALL x.P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))"; by Tac.depth; showResult(); (*An example of why exists_intr should be delayed as long as possible*) goal "(P --> (EX x.Q(x))) & P --> (EX x.Q(x))"; by Tac.depth; showResult(); (*instantiation of the variable ?a *) goal "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"; by Tac.depth; showResult(); goal "(ALL x. Q(x)) --> (EX x. Q(x))"; by Tac.depth; showResult(); print"Classical Logic: examples with quantifiers.\n"; goal "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"; by Tac.depth; showResult(); goal "(EX x. P-->Q(x)) <-> (P --> (EX x.Q(x)))"; by Tac.depth; showResult(); goal "(EX x.P(x)-->Q) <-> (ALL x.P(x)) --> Q"; by Tac.depth; showResult(); goal "(ALL x.P(x)) | Q <-> (ALL x. P(x) | Q)"; by Tac.depth; showResult(); print"Harder proofs \n"; (*This Prolog program needs multiple instantiation of ALL. *) goal "(ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"; by Tac.depth; (***or by (repeat (Tac.safeStep 1 || unify 1 || Rule.allL 1)); ***) showResult(); (*Needs double instantiation of EXISTS*) goal "EX x. P(x) --> P(a) & P(b)"; by Tac.depth; showResult(); goal "EX z. P(z) --> (ALL x. P(x))"; by Tac.depth; showResult(); print"Some slow ones\n"; (*Principia Mathematica *11.53 *) goal "(ALL x. ALL y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"; by Tac.depth; showResult(); (*Principia Mathematica *11.55 *) goal "(EX x. EX y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"; by Tac.depth; showResult(); (*Principia Mathematica *11.61 *) goal "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"; by Tac.depth; showResult(); (*Principia Mathematica *11.71 SLOW*) goal "(EX z. P(z)) & (EX w. Q(w)) --> \ \ ((ALL z. P(z) --> R(z)) & (ALL w. Q(w) --> S(w)) \ \ <-> (ALL z. ALL w. P(z) & Q(w) --> R(z) & S(w)))"; by Tac.depth; showResult(); (*from Vladimir Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23*) goal "EX x. EX X. ALL y. EX z. EX Z. \ \ (~P(y,y) | P(x,x) | ~S(z,x)) & \ \ (S(x,y) | ~S(y,z) | Q(Z,Z)) & \ \ (Q(X,y) | ~Q(y,Z) | S(X,X))"; (*Sample problems from F. J. Pelletier, Seventy-Five Problems for Testing Automatic Theorem Provers, J. Automated Reasoning 2 (1986), 191-216. Errata, JAR 4 (1988), 236-236. *) print"Pelletier's examples\n"; (*1*) goal "(P-->Q) <-> (~Q --> ~P)"; by Tac.depth; showResult(); (*2*) goal "~ ~ P <-> P"; by Tac.depth; showResult(); (*3*) goal "~(P-->Q) --> (Q-->P)"; by Tac.depth; showResult(); (*4*) goal "(~P-->Q) <-> (~Q --> P)"; by Tac.depth; showResult(); (*5*) goal "((P|Q)-->(P|R)) --> (P|(Q-->R))"; by Tac.depth; showResult(); (*6*) goal "P | ~ P"; by Tac.depth; showResult(); (*7*) goal "P | ~ ~ ~ P"; by Tac.depth; showResult(); (*8. Peirce's law*) goal "((P-->Q) --> P) --> P"; by Tac.depth; showResult(); (*9*) goal "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"; by Tac.depth; showResult(); (*10*) goal "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"; by Tac.depth; showResult(); (*11. Proved in each direction (incorrectly, says Pelletier!!) *)