Technische Universität München, Institut für Informatik
Lehrstuhl Informatik VIII, Rechnerarchitektur, Rechnerstruktur

The Theorem Prover

S E T H E O

Setheo is a fully automatic theorem prover for proving the unsatisfiability of formulae in first-order clause logic. The calculus underlying the system is model elimination respectively the connection tableau calculus. In contrast to systems based on resolution, the system is compatible and intended to be combined with goal-orientedness, i.e., the strategy to reason backward from the negation of the theorem to be proven. See
R. Letz and G. Stenz: Model Elimination and Connection Tableau Procedures
for a detailed description of the latest technology underlying the system.

A short history of the system

Originally, Setheo (for SEquential THEOrem prover) was developed as part of the theorem prover PARTHEO (for PARallel THEOrem prover) in a project funded by the Commission European Communities which was running from the end of the eighties to the beginning of the nineties. Then the efforts were reinforced in a project belonging to the Schwerpunkt Deduktion, a collection of closely coupled projects, funded by a special program of the Deutsche Forschungsgemeinschaft (DFG). Its general aim was to combine and further explore methods and systems for deduction. A goal of our group was to study the large variety of different types of logic, calculi, formalisms, methods of representation, and techniques for implementation. From comparisons of these methods and techniques, a number of new features like constraints and bottom-up reasoning methods were integrated in the backward oriented proof methodology of Setheo. Special emphasis was put on a high performance implementation of the system. After the end of this initiative, currently we are working on the development of techniques for the efficient handling of equality, which is pursued in the project E-SETHEO, also funded by the DFG.

Concerning implementation, there exist two lines of development. The older version (e.g. reference SETHEO V3.3 of January 1996) is implemented in C as an interpreter for abstract machine code similar to the typical manner a Prolog interpreter is realised. For this purpose, there exist two main programs, the compiler (inwasm) from logical notation to abstract machine code and the interpreter (sam). This system was also intended to be used for different extensions of the logic programming paradigm.
In the last years, the system has undergone a phase of complete redesign. After analysing the typical behaviour of the calculus on theorem proving applications, we have decided to give up the abstract machine paradigm and use a simpler and more modular architecture, which is also better suited for extensions of the calculus. High performance is achieved by a re-use technology (as described in the paper above). The current system is implemented in the scheme dialect bigloo. Although this implementation is much simpler and more robust concerning extensions, because of the employed re-use technology, the inference rates achieved on typical examples are even slightly higher than for the old implementation.

SETHEO is a project of the

Research Group 'Automated Reasoning'

Setheo-Bibliography

Tools for SETHEO: DataBase FrameWork (DBFW)

A short (ascii) description of the input langage can be found here, a gzipped PostScript file here.

About the older versions Setheo V3.2 and Setheo V3.0.

How to get the binaries:

SchemeSetheo is available for the following platforms:

SETHEO V3.3 is available for the following platforms:

You get there the binaries compiled for the appropriate operating system together with a set of example problems. It should be useful to have a look at the README file

To obtain the sources of SETHEO contact us, we will make the access to the code possible then. If you could compile the programmes on your computer, please let us know that. If you had some problems, give us some information about, too. If you ported SETHEO to another platform, please mail us the changes you had to made.

Of course, we improve SETHEO between new releases, too. Patches, new scripts and related things can be obtained here in the patches directory of our ftp server.

SETHEO V3.3 can also be obtained via FTP as follows:

        % ftp www8.informatik.tu-muenchen.de

        Name: anonymous
        Password: <your-e-mail-address>

        ftp> cd /pub/Automated_Reasoning/SETHEO
        ftp> binary

Then you can send a request for the file you want to get with one of the following commands.

        ftp> get setheo.solaris.tar.gz  
        ftp> get setheo.sunos.tar.gz  
        ftp> get setheo.hp.tar.gz  
        ftp> get setheo.linux.tar.gz  
        ftp> get setheo.FreeBSD-2.2.tar.gz  
        ftp> get README

Then quit the ftp connection.

         
        ftp> quit

If you have any further questions please contact

        EMAIL: setheo@informatik.tu-muenchen.de

        SNAIL: Gernot Stenz
               Technische Universitüt München
               Lehrstuhl VIII für Informatik / AR
               D-80290 München
               Germany

Changes:

Reinhold Letz, 04.03.02
Christian Gresser, 23.03.1994, 18.10.1994
Max Moser, 13.06.94, 28.06.94
Andreas Wolf, 1995-11-07, 1996-01-15
Ortrun Ibens, 1997-09-18, 1997-10-20, 1997-12-19