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.