From: "Eric J. Forbis" Subject: Logic software To: Josef Eschgfaeller I've received a steady stream of requests for information about theorem provers in response to my request on the APA BBS; below is a list of the programs I've seen thusfar. Pretty skimpy, I'm afraid. Several logic/AI conventions are being held this summer (notices have been posted on this list), which may make it easier to track down programs. Commercial programs are unintentionally underrepresented. If you're aware of other programs, public or commercial, please drop a note or update the list. Logic programs and teaching aids, theorem provers and languages. 1. MacLogic Uses symbolic logic notation. Working demo of classical logic for Macs, modal logic disabled. ftp.st-and.ac.uk 2. *Nqthm Boyer- Moore theorem prover (see book by same authors). Rascal.ics.utexas.edu :/pub/nqthm 3. *Proof-checker rascal.ics.utexas.edu :/pub/proof-checker 4. *Otter Herky.cs.uiowa.edu :/public/otter 5. *DTP meta.stanford.edu :/pub/dtp 6. **Setheo flop.informatik.tu-muenchen.de :/pub/fki 7. *HOL (Higher Order Language) ftp.cs.tut.fi :/pub/src/DisCo/hol90.6 Used to be available from ftp.uidaho.edu :/pub/hol, but didn't see it there 2/94 8. LogicWorks College level intro logic, commercial program. 700 Excersizes and programs, $18 demo (?), DOS 2.0+ Philosophical Documentation Center Bowling Green State University Bowling Green, OH 43403-0189 (800) 444-2419 9. Logic: A Workbook Teaches college level symbolic logic Commercial, price unknown, DOS 2.0+ Logic Software Project Department of Philosophy University of California, Los Angeles Los Angeles, CA 90024-1451 (213) 825-4641 * Requires LISP. Kyoto Common Lisp seems to be widely compatible with most of the above. It's conveniently available from rascal.ics.utexas.edu, amoung many other sites, and is available on all platforms. ** Requires Scheme. Available at this site (flop.informatik....). Items untrackable thusfar: NuPRL (by Martin & Lof) PTTP * * * Regards, -=-=-=-=-=-=-=-=-=-=-=-= Eric J. Forbis forb0004@gold.tc.umn.edu --- The High Performance Theorem Prover *** S E T H E O *** After several new developments concerning SETHEO and its components we are now able to provide the modified and updated version SETHEO V3.0 . SETHEO V3.0 consists of a set of binaries for Sun Sparc computers, manpages, and a set of example problems. SETHEO V3.0 can be obtained via FTP as follows: % ftp 131.159.8.35 (or "ftp flop.informatik.tu-muenchen.de") Name: anonymous Password: ftp> cd pub/fki ftp> binary ftp> get setheo.info ftp> get setheo.tar.Z ftp> bye If you have any further questions please contact EMAIL: setheo@informatik.tu-muenchen.de SNAIL: Intellektik Attn. M. Moser Technische Universitaet Muenchen Institut fuer Informatik Augustenstr. 46 RGB 8000 Muenchen 2 Germany Good Luck, and much fun with SETHEO About SETHEO: ============ SETHEO [Letz1992] is an automated theorem prover for formulae of predicate logic. The first version of this SEquential THEOrem prover was developed in the ESPRIT-project 415 ''Parallel Architectures and Languages for Advanced Information Processing'' at the chair of computer architecture of the Institut f"ur Informatik at the Technical University Munich. SETHEO is based on the calculus of so called ``connection tableaux'', which can be seen as an efficient integration of the tableau calculus [Smullyan1968], model elimination [Loveland1968] and the connection method [Bibel1987] and is very well suited for automated theorem proving. The way SETHEO works differs basically from that of traditional resolution based theorem provers and its today best known protagonist OTTER [McCune1988]. While resolution based theorem provers ensure the finding of a proof by some kind of breadth-first-search, SETHEO performs depth-first-search controlled by backtracking. In order to ensure the completeness of the proof procedure, in each `iteration' just finite parts of the search space are explored which are systematically increased in case of no success. This technique, commonly called `iterative deepening', was first implemented in the PTTP system of Stickel [Stickel1988]. The basic concept --`proof enumeration' instead of `formula enumeration'-- allows to use extremely refined variants of the calculus offering thus stronger search space reductions. Due to the success of prototypical versions of these refined variants, which has been proven in many experiments, we have decided to integrate them into the new system, SETHEO 3.0, which has been released in the spring of 93. SETHEO 3.0 provides `constraint techniques' which allow to impose structural restrictions on proofs in the model elimination calculus, the basic calculus of our system. The new techniques guarantee that in the proofs to be constructed no clause is used in a tautological instance, nor in a instance which can be subsumed. Furthermore the so called `regularity condition' ensures that all the literals in a path of a final tableau are different, thus reducing considerably the search space. By using `antilemma constraints' repeated solutions of subgoals resulting in the same answer substitution are avoided. The constraints we use can be seen as disequations of termlists. Whenever a variable is instantiated during the proof process, the relevant constraints for the variable are inspected and updated. The constraint checks are incorporated very elegantly into the unification subroutine of our prover. For efficiency the constraint set is always kept in `solved form', i.e. all the constraints belonging to the variables can be accessed very quickly. Constraints which no longer be violated are dynamically removed from the constraint set. The above techniques ensure that far less proofs have to be enumerated, and lots of infinite branches of the search space are eliminated. Tautology and subsumption constraints for the clauses are automatically generated in a preprocessing phase. The so called regularity constraints, however, and the antilemma constraints have to be generated dynamically during the proof search. However, constraints can be also added to the clauses of the input formula. This together with the concept of `global variables' (with destructive assignment) may be useful if you plan to use SETHEO as a tool for logic programming. In contrast to assert and retract in Prolog SETHEO's global variables have a clear decarative semantics. The global variables can be used to describe `changing worlds'. They are are automatically backtracked during the proof search. The final proof which eventually expresses a plan can be visualized by a proof display program. To achieve high efficiencey the main proof procedure of SETHEO is based on a Prolog-like compilation technique. The input formulae are transformed into instructions of an abstract register-based machine. The underlying abstract machine is an extension and a modified variant of the `Warren Abstract Machine' [Warren1983] as it is used in many professional Prolog systems today. Due to its highly efficient technique of implementation, SETHEO attains inference rates up to 70000 per second on standard sequential hardware (SUN Sparc 1 Workstation). The system developed so far can be seen as an intermediate version. In the future we plan to integrate a more powerful constraint generation module in preprocessing phase. In order to get shorter proofs we plan to use lemmata - and last not least more intelligent search techniques have to be implemented to improve the naive `iterative deepening' approach. Bibliography: ============= [Bibel1987] W.~Bibel. Automated Theorem Proving. Vieweg Verlag, Braunschweig, second edition, 1987. [Letz1992] R.~Letz, J.~Schumann, S.~Bayerl, and W.~Bibel. SETHEO: A High-Performance Theorem Prover. Journal of Automated Reasoning, 8(2):183--212, 1992. [Loveland1968] D.~W.~Loveland. Mechanical Theorem Proving by Model Elimination. Journal of the Association for Computing Machinery, 15(2):236--2 51, 1968. [McCune1988] W.~McCune. OTTER Users' Guide. Technical report, Mathematics and Computer Sci. Division, Argonne National Laboratory, Argonne, Ill., USA, May 1988. [Smullyan1968} R.~M.~Smullyan. First Order Logic. Springer, 1968. {Stickel1988] M.~A.~Stickel. A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. Journal of Automated Reasoning, 4:353--380, 1988. [Warren1983} D.~H.~D. Warren. An Abstract PROLOG Instruction Set. Technical report, SRI, Menlo Park, California, USA, 1983. --- Below is an abridged, intermediate version of the list of educational logic programs and theorem provers I recently posted. Several new entries have been added, and an address (MacLogic) corrected. I hope to add at least 4 new entries in the near future, straighten up the format, obtain addresses, add a paragraph- long description for each entry, and add a 3rd section listing professional journals that advertise or review logic software. If you're aware of programs that should be included, addresses, or are able to comment on the programs, please send email. -----Begin abridged list------------------------------- Logic programs and teaching aids, theorem provers and languages. =-=-=-Public Domain Programs-- most are theorem provers.=-=-=-=-=-=-=-= 1. PROOFCHK For use with the Shaum's _Outline of Logic_, natural deduction. Student enters proof and the theorem prover (a help button) offers graded series of hints for solutions. Also includes a validity checker and help screens. Send a disk and self- addressed stamped mailer to: John Nolt Philosophy Department University of Tennessee Knoxville, TN 37996-0480 2. *Nqthm Boyer- Moore theorem prover (see book by same authors). Rascal.ics.utexas.edu :/pub/nqthm 3. *Proof-checker rascal.ics.utexas.edu :/pub/proof-checker 4. *Otter Herky.cs.uiowa.edu :/public/otter 5. *DTP meta.stanford.edu :/pub/dtp 6. **Setheo flop.informatik.tu-muenchen.de :/pub/fki 7. *HOL (Higher Order Language) ftp.cs.tut.fi :/pub/src/DisCo/hol90.6 Used to be available from ftp.uidaho.edu :/pub/hol, but didn't see it there 2/94 8. MacLL "MacLogic-like proof editor for linear logic", by Roy Dyckhoff and the MALT (Machine Assisted Logic Teaching) project at St. Andrew's University. 138.251.192.40 (tamdhu.dcs.st-and.ac.au) :/pub/malt/macLL. Also get MacLogic fonts from /pub/malt/maclogic. * Requires LISP. Kyoto Common Lisp seems to be widely compatible with most of the above. It's conveniently available from rascal.ics.utexas.edu, amoung many other sites, and has been ported to most operating systems. ** Requires Scheme. Available at this site (flop.informatik....). =-=-=-Commercial Programs-- Both educational and theorem provers.=-=-=- Most of these use symbolic logic notation, rather than lisp or prolog. 1. MacLogic Minimal, intuitionistic, classical propositional & predicate calculi, with theorem provers. Macintosh Contact Roy Dyckhoff, the author, at rd@dcs.st-and.ac.uk for an informational sheet with directions for ftping. 2. LogicWorks College level intro logic. 700 Excersizes and programs, $18 demo (?), DOS 2.0+ Philosophical Documentation Center Bowling Green State University Bowling Green, OH 43403-0189 (800) 444-2419 3. Logic: A Workbook Teaches college level symbolic logic. Price unknown, DOS 2.0+. Logic Software Project Department of Philosophy University of California, Los Angeles Los Angeles, CA 90024-1451 (213) 825-4641 4. LogicCoach Educational software for the Hurley and Kahane logic texts. User friendly proof checker through 1st order functional calculus w/identity. Distributed by the Wadsworth Publishing Company. 5. Symlog College level symbolic logic educational software designed to be used with _Logic with Symlog_, Frederic Portoraro and Robert Tulley. Distributed by Prentice- Hall. 6. Tarski's World 4.0 1st order logic educational software to supplement any standard logic text. Represents logical propositions in graphical worlds, manual and exercises. By Jon Barwise and John Etchemendy. Macintosh and Windows, $19.50 Distributed by the University of Chicago Press. For more information, contact Dean Blobaum at dblobaum@press.uchicago.edu. 7. The Language of First- Order Logic_, 3rd edition. A 1st order symbolic logic text that includes Tarski's World 4.0. Macintosh and Windows, $34.95 Distributed by the University of Chicago Press. For more information, contact Dean Blobaum at dblobaum@press.uchicago.edu. 8. Turing's World 3.0: Introduction to Computability Theory Software for diagramming Turing machines, includes short text on Turing machines with software- integrated exercises. Macintosh, $19.95 Distributed by the University of Chicago Press. For more information, contact Dean Blobaum at dblobaum@press.uchicago.edu. 9. Hyperproof Text and software for analytic reasoning, can be used with items 6 and 7 in this section. "Combines graphical and sentential information, and presents a set of logical rules for integrating these different forms of information." Macintosh, $24.95 Distributed by the University of Chicago Press. For more information, contact Dean Blobaum at dblobaum@press.uchicago.edu. Unknown programs: NuPRL (by Martin & Lof) PTTP =-=-=-=-=Journals=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- 1. Philosophy and Computer Newsletter Carnegie Mellon University ------------End abridged list------------------------------- -=-=-=-=-=-=-=-=-=-=-=-= Eric J. Forbis forb0004@gold.tc.umn.edu ---