SETHEO Version 3.0

Appeared in Volume 8/3, August 1993

SETHEO [Letz1992] is an automated theorem prover for formulae of predicate logic. SETHEO (for SEquential THEOrem prover) has been developed in the ESPRIT project 415 'Parallel Architectures and Languages for Advanced Information Processing' at the chair of computer architecture of the Institut für Informatik at the Technical University Munich. SETHEO is based on 'connection tableaux' calculus, which can be seen as an efficient integration of the tableau calculus, model elimination, and the connection method.

The way SETHEO works differs from that of traditional resolution based theorem provers, and its best known protagonist OTTER [McCune1988]. While resolution based theorem provers ensure the discovery of a proof (thus guaranteeing 'strong' completeness) by some kind of breadth-first search, SETHEO performs depth-first search controlled by backtracking. In order to ensure strong completeness, finite parts of the search space are explored, the size being systematically increased until success (this approach is called 'iterative deepening').

Due to its highly efficient implementation, SETHEO can attain 70,000 inferences per second on standard sequential hardware (a SUN Sparc 1 Workstation).

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

[McCune1988] W. McCune. OTTER Users' Guide. Technical report, Mathematics and Computer Sci. Division, Argonne National Laboratory, Argonne, Ill., USA, May 1988.

SETHEO V3.0 consists of a set of binaries for Sun Sparc computers, manpages, and a set of example problems. These can be obtained via FTP from: ftp://flop.informatik.tu-muenchen.de/pub/fki

The relevant files are: setheo.info and setheo.tar.Z.

If you have any further questions please contact:

Intellektik
Attn. M. Moser
Technische Universitaet Muenchen
Augustenstr. 46 RGB
8000 Muenchen 2, Germany
Email: setheo@informatik.tu-muenchen.de