Technische Universität München, Fakultät für Informatik
Lehrstuhl Informatik IV, Research Group Automated Reasoning

E-SETHEO

E-SETHEO is a strategy-parallel compositional theorem prover for first-order logic with equality. It combines a variety of high-performance theorem provers and specialized decision procedures into one of the most powerful ATP systems currently available. The core idea of the E-SETHEO framework is to let different proof search procedures compete for resources for solving a given problem. E-SETHEO has won a number of prices for performance (but none for user-friendliness ;-).

Overview

E-SETHEO utilizes a number of different inference engines build on different calculi and using different heuristics.There are two distinct modes for the prover: Training mode and application mode. In application mode, the prover is fully automatic. It runs through three different phases: In training mode, some minimal user interaction is necessary. Training consists of a single complex step (involving normalization and classification for whole problem sets): The following paragraphs describe these phases:

Problem normalization

In a first step, the problem format is recognized, and the problem is transformed into clause normal form. Moreover, this CNF problem is further simplified as much as possible. The result is a representation of the proof problem in a format that is (after possible trivial transformations) accessible to all of our general purpose inference engines.

CNF transformation used to be done by FLOTTER, part of the SPASS system developed at the MPI für Informatik in Saarbrücken. We have now replaced SPASS with the new CNF converter in our own system E, making E-SETHEO a fully home-grown system.

Problem classification and schedule selection

In the second phase, the problem is classified according to a number of simple problem properties: Is the problem a unit problem (contains only clauses with one literal), Horn, or does it contain general clauses? Does the equality predicate occur? Is the problem from one of the classes for which the prover has a decision procedure? For each of the resulting classes, the prover selects a different schedule for the strategies. Such a schedule contains of a list of tuples (strategy, time limit), such that the sum over all individual time limits is equal to the total time limit for each proof attempt.

Proof search

In the final phase, the prover runs each strategy with the allocated time limit. It stops as soon as one of the strategies can determine the problem status (either by finding a proof or by showing that the problem does not have a proof). In principle, the strategies can run in parallel, either on a single processor, on an SMP system, or on a whole cluster of workstations. However, in our experience the overhead for problem distribution and the large maintainance effort for the parallel version does not pay off. Our current implementation therefore sequentializes the proof search, i.e. strategies are attempted one after the other in a fixed order.

Schedule optimization

It is well-known that different application domains require very different proof search strategies. In order to adapt E-SETHEO to a given domain, all strategies are run on a representative sample of problems. We then apply a combination of genetic optimization and hill-climbing to find an (approximately) optimal set of schedules for this sample. If the sample is well-chosen (or plain large enough), the generated schedules usually show an excellent performance over the whole domain.

Individual Strategies

The success of E-SETHEO can be partially explained by the concept of strategy parallelism and the easy adaption to a given application domain. However, another major reason is the number of excellent inference engines used for the different strategies. E-SETHEO employs first-order provers based on three very different paradigms. Each of these provers is among the top-performing systems in its class. In addition, E-SETHEO also uses special decision procedures for propositional and finitely groundable problems, as well as cooperative strategies build on lemma exchange between different systems.

Getting E-SETHEO

While E-SETHEO is a powerful system, it still is very prototypical in nature. The components are written in many different programming languages, and are available under different licenses. Moreover, there are significant external software requirements, including gcc, Perl, Eclipse Prolog, Bigloo Scheme, and suitable UNIX tools. For this reasons, we do not offer E-SETHEO for download. If you urgently need to use the system, please send us an email, and we can hopefully work something out. If you just need to prove a small number of problems, please consider Geoff Sutcliffe's SystemOnTPTP.
Stephan Schulz,schulz@informatik.tu-muenchen.de, 5.7.2000