1(**** Test Data for Chapter 10 of 2 3 ML for the Working Programmer, 2nd edition 4 by Lawrence C. Paulson, Computer Laboratory, University of Cambridge. 5 (Cambridge University Press, 1996) 6 7Copyright (C) 1996 by Cambridge University Press. 8Permission to copy without fee is granted provided that this copyright 9notice and the DISCLAIMER OF WARRANTY are included in any copy. 10 11DISCLAIMER OF WARRANTY. These programs are provided `as is' without 12warranty of any kind. We make no warranties, express or implied, that the 13programs are free of error, or are consistent with any particular standard 14of merchantability, or that they will meet your requirements for any 15particular application. They should not be relied upon for solving a 16problem whose incorrect solution could result in injury to a person or loss 17of property. If you do use the programs or functions in such a manner, it 18is at your own risk. The author and publisher disclaim all liability for 19direct, incidental or consequential damages resulting from your use of 20these programs or functions. 21****) 22 23 24open Command; 25open Tactical; 26 27fun showResult () = 28 if Rule.final(getState()) then DisplayFol.form(Rule.main (getState())) 29 else raise Fail "Unsolved subgoals exist!"; 30 31fun checkFailed() = 32 if Rule.final(getState()) then raise Fail "Should have failed!" 33 else "Failed, as expected..."; 34 35(*** Single step proofs and basic use of tacticals ***) 36 37(*single steps -- essentially the proof * of section 10.2 *) 38goal "P & Q --> Q & P"; 39by (Rule.impR 1); 40by (Rule.conjL 1); 41by (Rule.conjR 1); 42by (Rule.basic 2); 43by (Rule.basic 1); 44showResult(); 45 46(* essentially the first quantifier proof, section 10.4 *) 47goal "(ALL x.P(x)) --> (ALL x. P(x) | Q(x))"; 48by (Rule.impR 1); 49by (Rule.allR 1); 50by (Rule.disjR 1); 51by (Rule.allL 1); 52by (Rule.unify 1); 53showResult(); 54 55 56(* the second quantifier proof, section 10.4 *) 57goal "EX z. P(z) --> (ALL x. P(x))"; 58by (Rule.exR 1); 59by (Rule.impR 1); 60by (Rule.allR 1); 61by (Rule.unify 1); (*FAILS!*) 62by (Rule.exR 1); 63by (Rule.impR 1); 64by (Rule.unify 1); 65showResult(); 66 67 68 69goal "(P & Q) & R --> P & (Q & R)"; 70by (Rule.impR 1); 71by (Rule.conjL 1); 72by (Rule.conjL 1); 73by (Rule.conjR 1); 74by (Rule.conjR 2); 75by (Rule.basic 1); 76by (Rule.basic 1); 77by (Rule.basic 1); 78showResult(); 79 80(** Demonstrating tacticals **) 81 82goal "(P & Q) & R --> P & (Q & R)"; 83by (repeat (Rule.impR 1 || Rule.conjL 1)); 84by (repeat (Rule.basic 1 || Rule.conjR 1)); 85showResult(); 86 87 88goal "EX z. P(z) --> (ALL x. P(x))"; 89by (repeat (Rule.unify 1 || Rule.impR 1 || 90 Rule.allR 1 || Rule.exR 1)); 91showResult(); 92 93(*single steps*) 94goal "(P & Q) | R --> (P | R) & (Q | R)"; 95by (Rule.impR 1); 96by (Rule.disjL 1); 97by (Rule.conjL 1); 98by (Rule.conjR 1); 99by (Rule.disjR 1); 100by (Rule.disjR 2); 101by (Rule.conjR 3); 102by (Rule.disjR 3); 103by (Rule.disjR 4); 104by (Rule.basic 1); 105by (Rule.basic 1); 106by (Rule.basic 1); 107by (Rule.basic 1); 108showResult(); 109 110 111(*single steps*) 112goal "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"; 113by (Rule.iffR 1); 114by (Rule.conjR 1); 115by (Rule.allR 1); 116by (Rule.allL 1); 117by (Rule.conjL 1); 118by (Rule.unify 1); 119by (Rule.allR 1); 120by (Rule.allL 1); 121by (Rule.conjL 1); 122by (Rule.unify 1); 123by (Rule.allR 1); 124by (Rule.conjL 1); 125by (Rule.allL 1); 126by (Rule.allL 1); 127by (Rule.conjR 1); 128by (Rule.unify 1); 129by (Rule.unify 1); 130showResult(); 131 132goal "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"; 133by (repeat (Rule.unify 1 || Rule.iffR 1 || Rule.allR 1 134 || Rule.conjR 1 || Rule.conjL 1 135 || Rule.allL 1)); 136showResult(); 137 138 139(*single steps -- BASIC TEST OF QUANTIFIER REASONING *) 140goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; 141by (Rule.impR 1); 142by (Rule.exL 1); 143by (Rule.allR 1); 144by (Rule.allL 1); 145by (Rule.exR 1); 146by (Rule.unify 1); 147showResult(); 148 149 150(*single steps -- BASIC TEST OF QUANTIFIER REASONING -- INVALID *) 151goal "(ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"; 152by (Rule.impR 1); 153by (Rule.allL 1); 154by (Rule.exL 1); 155by (Rule.exR 1); 156by (Rule.allR 1); 157by (Rule.unify 1); 158checkFailed(); 159(*NB. The failure of this proof does not demonstrate that no proof exists!*) 160 161 162goal "(EX x.P(x)-->Q) <-> (ALL x.P(x)) --> Q"; 163by (Rule.iffR 1); 164by (Rule.impR 1); 165by (Rule.exL 1); 166by (Rule.allL 1); 167by (Rule.impL 1); 168by (Rule.unify 1); 169by (Rule.unify 1); 170by (Rule.impL 1); 171by (Rule.exR 1); 172by (Rule.impR 1); 173by (Rule.unify 1); 174by (Rule.allR 1); 175by (Rule.exR 1); 176by (Rule.impR 1); 177by (Rule.unify 1); 178showResult(); 179 180 181(*** Automatic proofs ***) 182 183print"commutative laws of & and | \n"; 184goal "P & Q --> Q & P"; 185by Tac.depth; 186showResult(); 187 188goal "P | Q --> Q | P"; 189by Tac.depth; 190showResult(); 191 192 193print"associative laws of & and | \n"; 194goal "(P & Q) & R --> P & (Q & R)"; 195by Tac.depth; 196showResult(); 197 198goal "(P | Q) | R --> P | (Q | R)"; 199by Tac.depth; 200showResult(); 201 202 203print"distributive laws of & and | \n"; 204goal "(P & Q) | R --> (P | R) & (Q | R)"; 205by Tac.depth; 206showResult(); 207 208goal "(P | R) & (Q | R) --> (P & Q) | R"; 209by Tac.depth; 210showResult(); 211 212goal "(P | Q) & R --> (P & R) | (Q & R)"; 213by Tac.depth; 214showResult(); 215 216goal "(P & R) | (Q & R) --> (P | Q) & R"; 217by Tac.depth; 218showResult(); 219 220 221print"Laws involving implication\n"; 222 223goal "(P-->R) & (Q-->R) <-> (P|Q --> R)"; 224by Tac.depth; 225showResult(); 226 227goal "(P & Q --> R) <-> (P--> (Q-->R))"; 228by Tac.depth; 229showResult(); 230 231goal "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"; 232by Tac.depth; 233showResult(); 234 235goal "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"; 236by Tac.depth; 237showResult(); 238 239goal "(P --> Q & R) <-> (P-->Q) & (P-->R)"; 240by Tac.depth; 241showResult(); 242 243 244print"Propositions-as-types\n"; 245 246(*The combinator K*) 247goal "P --> (Q --> P)"; 248by Tac.depth; 249showResult(); 250 251(*The combinator S*) 252goal "(P-->Q-->R) --> (P-->Q) --> (P-->R)"; 253by Tac.depth; 254showResult(); 255 256(*Converse is classical*) 257goal "(P-->Q) | (P-->R) --> (P --> Q | R)"; 258by Tac.depth; 259showResult(); 260 261goal "(P-->Q) --> (~Q --> ~P)"; 262by Tac.depth; 263showResult(); 264 265 266print"Classical examples\n"; 267 268goal "(P --> Q | R) --> (P-->Q) | (P-->R)"; 269by Tac.depth; 270showResult(); 271 272(*If and only if*) 273 274goal "(P<->Q) <-> (Q<->P)"; 275by Tac.depth; 276showResult(); 277 278goal "~ (P <-> ~P)"; 279by Tac.depth; 280showResult(); 281 282 283print"*** Quantifier examples ***\n"; 284 285goal "(ALL x. ALL y.P(x,y)) --> (ALL y. ALL x.P(x,y))"; 286by Tac.depth; 287showResult(); 288 289goal "(EX x. EX y.P(x,y)) --> (EX y. EX x.P(x,y))"; 290by Tac.depth; 291showResult(); 292 293(*Converse is false*) 294goal "(ALL x.P(x)) | (ALL x.Q(x)) --> (ALL x. P(x) | Q(x))"; 295by Tac.depth; 296showResult(); 297 298goal "(ALL x. P-->Q(x)) <-> (P--> (ALL x.Q(x)))"; 299by Tac.depth; 300showResult(); 301 302 303goal "(ALL x.P(x)-->Q) <-> ((EX x.P(x)) --> Q)"; 304by Tac.depth; 305showResult(); 306 307 308print"Some harder ones\n"; 309 310goal "(EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))"; 311by Tac.depth; 312showResult(); 313 314(*Converse is false*) 315goal "(EX x. P(x)&Q(x)) --> (EX x.P(x)) & (EX x.Q(x))"; 316by Tac.depth; 317showResult(); 318 319 320print"Basic test of quantifier reasoning\n"; 321(*TRUE*) 322goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; 323by Tac.depth; 324showResult(); 325 326 327goal "(ALL x. Q(x)) --> (EX x. Q(x))"; 328by Tac.depth; 329showResult(); 330 331 332print"The following should fail, as they are false!\n"; 333 334goal "(EX x. Q(x)) --> (ALL x. Q(x))"; 335by Tac.depth; 336checkFailed(); 337 338goal "P(?a) --> (ALL x.P(x))"; 339by Tac.depth; 340checkFailed(); 341 342goal "(P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))"; 343by Tac.depth; 344checkFailed(); 345 346print"Back to things that are provable...\n"; 347 348goal "(ALL x.P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))"; 349by Tac.depth; 350showResult(); 351 352 353(*An example of why exists_intr should be delayed as long as possible*) 354goal "(P --> (EX x.Q(x))) & P --> (EX x.Q(x))"; 355by Tac.depth; 356showResult(); 357 358(*instantiation of the variable ?a *) 359goal "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"; 360by Tac.depth; 361showResult(); 362 363goal "(ALL x. Q(x)) --> (EX x. Q(x))"; 364by Tac.depth; 365showResult(); 366 367 368print"Classical Logic: examples with quantifiers.\n"; 369 370goal "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"; 371by Tac.depth; 372showResult(); 373 374goal "(EX x. P-->Q(x)) <-> (P --> (EX x.Q(x)))"; 375by Tac.depth; 376showResult(); 377 378goal "(EX x.P(x)-->Q) <-> (ALL x.P(x)) --> Q"; 379by Tac.depth; 380showResult(); 381 382goal "(ALL x.P(x)) | Q <-> (ALL x. P(x) | Q)"; 383by Tac.depth; 384showResult(); 385 386 387print"Harder proofs \n"; 388 389(*This Prolog program needs multiple instantiation of ALL. *) 390goal "(ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"; 391by Tac.depth; 392(***or 393by (repeat (Tac.safeStep 1 || unify 1 || Rule.allL 1)); 394***) 395showResult(); 396 397(*Needs double instantiation of EXISTS*) 398goal "EX x. P(x) --> P(a) & P(b)"; 399by Tac.depth; 400showResult(); 401 402goal "EX z. P(z) --> (ALL x. P(x))"; 403by Tac.depth; 404showResult(); 405 406 407print"Some slow ones\n"; 408 409(*Principia Mathematica *11.53 *) 410goal "(ALL x. ALL y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"; 411by Tac.depth; 412showResult(); 413 414 415(*Principia Mathematica *11.55 *) 416goal "(EX x. EX y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"; 417by Tac.depth; 418showResult(); 419 420 421(*Principia Mathematica *11.61 *) 422goal "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"; 423by Tac.depth; 424showResult(); 425 426 427(*Principia Mathematica *11.71 SLOW*) 428goal "(EX z. P(z)) & (EX w. Q(w)) --> \ 429\ ((ALL z. P(z) --> R(z)) & (ALL w. Q(w) --> S(w)) \ 430\ <-> (ALL z. ALL w. P(z) & Q(w) --> R(z) & S(w)))"; 431by Tac.depth; 432showResult(); 433 434 435(*from Vladimir Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23*) 436goal "EX x. EX X. ALL y. EX z. EX Z. \ 437\ (~P(y,y) | P(x,x) | ~S(z,x)) & \ 438\ (S(x,y) | ~S(y,z) | Q(Z,Z)) & \ 439\ (Q(X,y) | ~Q(y,Z) | S(X,X))"; 440 441 442(*Sample problems from 443 F. J. Pelletier, 444 Seventy-Five Problems for Testing Automatic Theorem Provers, 445 J. Automated Reasoning 2 (1986), 191-216. 446 Errata, JAR 4 (1988), 236-236. 447*) 448 449print"Pelletier's examples\n"; 450(*1*) 451goal "(P-->Q) <-> (~Q --> ~P)"; 452by Tac.depth; 453showResult(); 454 455(*2*) 456goal "~ ~ P <-> P"; 457by Tac.depth; 458showResult(); 459 460(*3*) 461goal "~(P-->Q) --> (Q-->P)"; 462by Tac.depth; 463showResult(); 464 465(*4*) 466goal "(~P-->Q) <-> (~Q --> P)"; 467by Tac.depth; 468showResult(); 469 470(*5*) 471goal "((P|Q)-->(P|R)) --> (P|(Q-->R))"; 472by Tac.depth; 473showResult(); 474 475(*6*) 476goal "P | ~ P"; 477by Tac.depth; 478showResult(); 479 480(*7*) 481goal "P | ~ ~ ~ P"; 482by Tac.depth; 483showResult(); 484 485(*8. Peirce's law*) 486goal "((P-->Q) --> P) --> P"; 487by Tac.depth; 488showResult(); 489 490(*9*) 491goal "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"; 492by Tac.depth; 493showResult(); 494 495(*10*) 496goal "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"; 497by Tac.depth; 498showResult(); 499 500(*11. Proved in each direction (incorrectly, says Pelletier!!) *) 501goal "P<->P"; 502by Tac.depth; 503showResult(); 504 505(*12. "Dijkstra's law"*) 506goal "((P <-> Q) <-> R) <-> (P <-> (Q <-> R))"; 507by Tac.depth; 508showResult(); 509 510(*13. Distributive law*) 511goal "P | (Q & R) <-> (P | Q) & (P | R)"; 512by Tac.depth; 513showResult(); 514 515(*14*) 516goal "(P <-> Q) <-> ((Q | ~P) & (~Q|P))"; 517by Tac.depth; 518showResult(); 519 520(*15*) 521goal "(P --> Q) <-> (~P | Q)"; 522by Tac.depth; 523showResult(); 524 525(*16*) 526goal "(P-->Q) | (Q-->P)"; 527by Tac.depth; 528showResult(); 529 530(*17*) 531goal "((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"; 532by Tac.depth; 533showResult(); 534 535 536print"Problem 18. \n"; 537goal "EX y. ALL x. P(y)-->P(x)"; 538by Tac.depth; 539showResult(); 540 541 542 543print"Problem 19. \n"; 544goal "EX x. ALL y. ALL z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"; 545by Tac.depth; 546showResult(); 547 548 549print"Problem 20. \n"; 550goal "(ALL x. ALL y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) \ 551\ --> (EX x. EX y. P(x) & Q(y)) --> (EX z. R(z))"; 552by Tac.depth; 553showResult(); 554 555 556 557print"Problem 21. \n"; 558goal "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))"; 559by Tac.depth; 560showResult(); 561 562 563print"Problem 22\n"; 564goal "(ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"; 565by Tac.depth; 566showResult(); 567 568 569print"Problem 23\n"; 570goal "(ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))"; 571by Tac.depth; 572showResult(); 573 574 575print"Problem 24\n"; 576goal "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \ 577\ (~(EX x.P(x)) --> (EX x.Q(x))) & (ALL x. Q(x)|R(x) --> S(x)) \ 578\ --> (EX x. P(x)&R(x))"; 579by Tac.depth; 580showResult(); 581 582 583print"Problem 25\n"; 584goal "(EX x. P(x)) & \ 585\ (ALL x. L(x) --> ~ (M(x) & R(x))) & \ 586\ (ALL x. P(x) --> (M(x) & L(x))) & \ 587\ ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) \ 588\ --> (EX x. Q(x)&P(x))"; 589by Tac.depth; 590showResult(); 591 592 593print"Problem 26\n"; 594goal "((EX x. p(x)) <-> (EX x. q(x))) & \ 595\ (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y))) \ 596\ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"; 597by Tac.depth; 598showResult(); 599 600 601print"Problem 27\n"; 602goal "(EX x. P(x) & ~Q(x)) & \ 603\ (ALL x. P(x) --> R(x)) & \ 604\ (ALL x. M(x) & L(x) --> P(x)) & \ 605\ ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) \ 606\ --> (ALL x. M(x) --> ~L(x))"; 607by (Tac.depthIt 5); 608showResult(); 609 610 611print"Problem 28. AMENDED\n"; 612goal "(ALL x. P(x) --> (ALL x. Q(x))) & \ 613\ ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & \ 614\ ((EX x.S(x)) --> (ALL x. L(x) --> M(x))) \ 615\ --> (ALL x. P(x) & L(x) --> M(x))"; 616by Tac.depth; 617showResult(); 618 619 620print"Problem 29. Essentially the same as Principia Mathematica *11.71\n"; 621goal "(EX x. P(x)) & (EX y. Q(y)) \ 622\ --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <-> \ 623\ (ALL x. ALL y. P(x) & Q(y) --> R(x) & S(y)))"; 624by Tac.depth; 625showResult(); 626 627 628print"Problem 30\n"; 629goal "(ALL x. P(x) | Q(x) --> ~ R(x)) & \ 630\ (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) \ 631\ --> (ALL x. S(x))"; 632by Tac.depth; 633showResult(); 634 635 636print"Problem 31. \n"; 637goal "~(EX x.P(x) & (Q(x) | R(x))) & \ 638\ (EX x. L(x) & P(x)) & \ 639\ (ALL x. ~ R(x) --> M(x)) \ 640\ --> (EX x. L(x) & M(x))"; 641by Tac.depth; 642showResult(); 643 644 645print"Problem 32. \n"; 646goal "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \ 647\ (ALL x. S(x) & R(x) --> L(x)) & \ 648\ (ALL x. M(x) --> R(x)) \ 649\ --> (ALL x. P(x) & M(x) --> L(x))"; 650by Tac.depth; 651showResult(); 652 653 654print"Problem 33\n"; 655goal "(ALL x. P(a) & (P(x)-->P(b))-->P(c)) <-> \ 656\ (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"; 657by Tac.depth; 658showResult(); 659 660print"Problem 34 AMENDED (TWICE!!)\n"; 661(*Andrews's challenge*) 662goal "((EX x. ALL y. p(x) <-> p(y)) <-> \ 663\ ((EX x. q(x)) <-> (ALL y. p(y)))) <-> \ 664\ ((EX x. ALL y. q(x) <-> q(y)) <-> \ 665\ ((EX x. p(x)) <-> (ALL y. q(y))))"; 666by Tac.depth; 667showResult(); 668 669 670print"Problem 35. \n"; 671goal "EX x. EX y. P(x,y) --> (ALL u. ALL v. P(u,v))"; 672by Tac.depth; 673showResult(); 674 675 676print"Problem 36. \n"; 677goal "(ALL x. EX y. J(x,y)) & \ 678\ (ALL x. EX y. G(x,y)) & \ 679\ (ALL x. ALL y. J(x,y) | G(x,y) --> \ 680\ (ALL z. J(y,z) | G(y,z) --> H(x,z))) \ 681\ --> (ALL x. EX y. H(x,y))"; 682by Tac.depth; 683showResult(); 684 685 686print"Problem 37\n"; 687goal "(ALL z. EX w. ALL x. EX y. \ 688\ (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \ 689\ (ALL x. ALL z. ~P(x,z) --> (EX y. Q(y,z))) & \ 690\ ((EX x. EX y. Q(x,y)) --> (ALL x. R(x,x))) \ 691\ --> (ALL x. EX y. R(x,y))"; 692by Tac.depth; 693showResult(); 694 695 696print"Problem 38. NOT PROVED\n"; 697goal "(ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) --> \ 698\ (EX z. EX w. p(z) & r(x,w) & r(w,z))) <-> \ 699\ (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) & \ 700\ (~p(a) | ~(EX y. p(y) & r(x,y)) | \ 701\ (EX z. EX w. p(z) & r(x,w) & r(w,z))))"; 702(*NOT PROVED*) 703 704print"Problem 39\n"; 705goal "~ (EX x. ALL y. J(x,y) <-> ~J(y,y))"; 706by Tac.depth; 707showResult(); 708 709 710print"Problem 40. AMENDED\n"; 711goal "(EX y. ALL x. J(y,x) <-> ~J(x,x)) --> \ 712\ ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"; 713by Tac.depth; 714showResult(); 715 716 717print"Problem 41\n"; 718goal "(ALL z. (EX y. (ALL x. f(x,y) <-> f(x,z) & ~ f(x,x)))) \ 719\ --> ~ (EX z. ALL x. f(x,z))"; 720by (Tac.depthIt 1); 721showResult(); 722 723 724print"Problem 42\n"; 725goal "~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))"; 726by (Tac.depthIt 5); 727showResult(); 728 729print"Problem 43 NOT PROVED\n"; 730goal "(ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y))) \ 731\ --> (ALL x. (ALL y. q(x,y) <-> q(y,x)))"; 732(*NOT PROVED*) 733 734print"Problem 44\n"; 735goal "(ALL x. f(x) --> \ 736\ (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \ 737\ (EX x. j(x) & (ALL y. g(y) --> h(x,y))) \ 738\ --> (EX x. j(x) & ~f(x))"; 739by Tac.depth; 740showResult(); 741 742 743print"Problem 45\n"; 744goal "(ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y)) \ 745\ --> (ALL y. g(y) & h(x,y) --> k(y))) & \ 746\ ~ (EX y. l(y) & k(y)) & \ 747\ (EX x. f(x) & (ALL y. h(x,y) --> l(y)) \ 748\ & (ALL y. g(y) & h(x,y) --> j(x,y))) \ 749\ --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))"; 750by Tac.depth; 751showResult(); 752 753 754print"Problem 46\n"; 755goal "(ALL x. f(x) & (ALL y. f(y) & h(y,x) --> g(y)) --> g(x)) & \ 756\ ((EX x.f(x) & ~g(x)) --> \ 757\ (EX x. f(x) & ~g(x) & (ALL y. f(y) & ~g(y) --> j(x,y)))) & \ 758\ (ALL x. ALL y. f(x) & f(y) & h(x,y) --> ~j(y,x)) \ 759\ --> (ALL x. f(x) --> g(x))"; 760by Tac.depth; 761showResult(); 762 763 764(* Example suggested by Johannes Schumann and credited to Pelletier *) 765goal "(ALL x. ALL y. ALL z. P(x,y) --> P(y,z) --> P(x,z)) --> \ 766\ (ALL x. ALL y. ALL z. Q(x,y) --> Q(y,z) --> Q(x,z)) --> \ 767\ (ALL x. ALL y.Q(x,y) --> Q(y,x)) --> \ 768\ (ALL x. ALL y. P(x,y) | Q(x,y)) --> \ 769\ (ALL x. ALL y.P(x,y)) | (ALL x. ALL y.Q(x,y))"; 770(*NOT PROVED*) 771 772print"Problem 47 Schubert's Steamroller\n"; 773goal "(ALL x. P1(x) --> P0(x)) & (EX x.P1(x)) & \ 774\ (ALL x. P2(x) --> P0(x)) & (EX x.P2(x)) & \ 775\ (ALL x. P3(x) --> P0(x)) & (EX x.P3(x)) & \ 776\ (ALL x. P4(x) --> P0(x)) & (EX x.P4(x)) & \ 777\ (ALL x. P5(x) --> P0(x)) & (EX x.P5(x)) & \ 778\ (ALL x. Q1(x) --> Q0(x)) & (EX x.Q1(x)) & \ 779\ (ALL x. P0(x) --> ((ALL y.Q0(y)-->R(x,y)) | \ 780\ (ALL y.P0(y) & S(y,x) & \ 781\ (EX z.Q0(z)&R(y,z)) --> R(x,y)))) & \ 782\ (ALL x. ALL y. P3(y) & (P5(x)|P4(x)) --> S(x,y)) & \ 783\ (ALL x. ALL y. P3(x) & P2(y) --> S(x,y)) & \ 784\ (ALL x. ALL y. P2(x) & P1(y) --> S(x,y)) & \ 785\ (ALL x. ALL y. P1(x) & (P2(y)|Q1(y)) --> ~R(x,y)) & \ 786\ (ALL x. ALL y. P3(x) & P4(y) --> R(x,y)) & \ 787\ (ALL x. ALL y. P3(x) & P5(y) --> ~R(x,y)) & \ 788\ (ALL x. (P4(x)|P5(x)) --> (EX y.Q0(y) & R(x,y))) \ 789\ --> (EX x. EX y. P0(x) & P0(y) & (EX z. Q1(z) & R(y,z) & R(x,y)))"; 790(*NOT PROVED*) 791 792 793print"Reached end of file.\n"; 794