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.