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
---