XEROX BOYERMOORE 2 4 1 BOYERMOORE 1 4 Our Theorem Prover By: R. S. Boyer and J Strother Moore Austin, Texas circa 1983 INTRODUCTION BY KELLY ROACH (Roach.pa@Xerox.com) This is the infamous Boyer-Moore Theorem Prover written by Boyer and Moore. I (Kelly Roach) have gone to the trouble of translating Boyer and Moore's theorem prover from Zetalisp into Interlisp-D in order to use it and understand it for my own enlightenment. I think others too would like to experiment with this classic program and so I have put my translation onto LISPUSERS. The short documentation is to LOAD BOYERMOORE.DCOM & BOYERMOOREDATA and do (PROVEALL1) [Function] (* Bootstrap the theorem prover. *) (PROVEALL2) [Function] (* Prove basic theorems & define some basic fns. *) The most important user interface functions are DEFN and PROVE-LEMMA. You can PP PROVEALL2 and see how I set up DEFN& and PROVE-LEMMA& to call DEFN and PROVE-LEMMA fairly directly. There are other PROVEALLi functions which I have not run as thoroughlyÿÿï%ÿI also need to undo a small amount of damage in some of the PROVEALLi for i>2 brought on by my translation. I'm going to try to get what official documentation I can at some point and modify it to be correct for Interlisp-D. Please direct any problems with this particular translation to ROACH.PA@XEROX.ARPA. The remainder of this document is general commentary excerpted from Boyer and Moore's own documentation. LANGUAGES AND MACHINES We began working on this code in 1972 in Edinburgh at the Metamathematics Unit. The first version was written in POP-2 for an ICL 4130. In Palo Alto in 1974 we translated it into Interlisp-10 for a Xerox MAXC and a DEC PDP10/BBN-TENEX. We continued developing it at Xerox PARC, SRI, and the University of Texas on two DEC-2060s. In 1983, we translated it into Maclisp for a DEC-2060 a Honeywell Multics and into Zetalisp for a Symbolics 3600. John Nagle made it compatible with Franz Lisp for the VAX. OWNERSHIP The development of this system has been primarily financed by the National Science Foundation and the Office of Naval Research. The NSF Grant Policy Manual NSF-77-47, Revised October 1979, states in paragraph 754.2 "Data banks and software, produced with the assistance of NSF grants, having utility to others in addition to the grantee, shall be made available to users, at no cost to the grantee, by publication or, on request, by duplication or loan for reproduction by others. ... Any out of pocket expenses incurred by the grantee in providing information to third parties may be charged to the third party. DOCUMENTATION The 1978 version of this system was carefully described in "A Computational Logic," Academic Press, 1979. But much has changed. (1) An extensive amount of "linear" arithmetic has been built-in. (2) We have added the notion of metafunctions described in "Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures" in "The Correctness Problem in Computer Science," R. S. Boyer and J S. Moore (editors), Academic Press, 1981. (3) Equality reasoning in the ground case is complete. (4) The mechanism for guessing well-founded relations at definition time has been vastly simplified but now requires more explicit guidance from the user in the nontrivial cases. (5) A variety of hints can be given to the theorem-prover. The user's manual for the 1978 version of the theorem-prover is extremely out of date. The best we can offer at this time is the file CODE.SUB, "A Poor Substitute for a User's Manual for a Theorem Prover for a Computational Logic." THE SYSTEM This code works in Maclisp on a DEC 2060 and on a Honeywell Multics, in Zetalisp on a Symbolics 3600, in Franz Lisp on Vaxes. (LIST ((PAGE NIL (PAPERSIZE Letter FOLIOINFO (ARABIC ) STARTINGPAGE# 1) (0 0 612 792) ((FOLIO NIL (PARALOOKS (QUAD CENTERED) CHARLOOKS (SUPERSCRIPT 0 INVISIBLE OFF SELECTPOINT OFF PROTECTED OFF SIZE 10 FAMILY MODERN OVERLINE OFF STRIKEOUT OFF UNDERLINE OFF EXPANSION REGULAR SLOPE REGULAR WEIGHT MEDIUM INVERTED OFF USERINFO NIL STYLE NIL) FORMATINFO (ARABIC )) (174 36 288 36) NIL) (HEADING NIL (HEADINGTYPE RUNNINGHEAD) (84 744 528 36) NIL) (TEXT NIL NIL (84 96 456 600) NIL))) (PAGE NIL (PAPERSIZE Letter FOLIOINFO (ARABIC )) (0 0 612 792) ((FOLIO NIL (PARALOOKS (QUAD CENTERED) CHARLOOKS (SUPERSCRIPT 0 INVISIBLE OFF SELECTPOINT OFF PROTECTED OFF SIZE 10 FAMILY MODERN OVERLINE OFF STRIKEOUT OFF UNDERLINE OFF EXPANSION REGULAR SLOPE REGULAR WEIGHT MEDIUM INVERTED OFF USERINFO NIL STYLE NIL) FORMATINFO (ARABIC )) (174 36 288 36) NIL) (HEADING NIL (HEADINGTYPE RUNNINGHEAD) (84 744 528 36) NIL) (TEXT NIL NIL (84 96 456 600) NIL))) (PAGE NIL (PAPERSIZE Letter FOLIOINFO (ARABIC )) (0 0 612 792) ((FOLIO NIL (PARALOOKS (QUAD CENTERED) CHARLOOKS (SUPERSCRIPT 0 INVISIBLE OFF SELECTPOINT OFF PROTECTED OFF SIZE 10 FAMILY MODERN OVERLINE OFF STRIKEOUT OFF UNDERLINE OFF EXPANSION REGULAR SLOPE REGULAR WEIGHT MEDIUM INVERTED OFF USERINFO NIL STYLE NIL) FORMATINFO (ARABIC )) (174 36 288 36) NIL) (HEADING NIL (HEADINGTYPE RUNNINGHEAD) (84 744 528 36) NIL) (TEXT NIL NIL (84 96 456 600) NIL)))))(È (È (ŠŠ8(ŠŠ8DÈÈ PAGEHEADING RUNNINGHEADMODERN MODERNLOGOMODERN MODERN   HRULE.GETFNMODERN  HRULE.GETFNMODERN  HRULE.GETFNMODERN   HRULE.GETFNMODERN  HRULE.GETFNMODERN 0;  %Ç!$!4ýÁü g óé ~úBzº