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:
- Problem normalization
- Problem classification and schedule selection
- (Strategy-parallel) proof search
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.
- SETHEO
SETHEO
is a theorem prover based on the model elimination
calculus. In E-SETHEO, various versions of SETHEO with different
search strategies and different preprocessing are used as
separate strategies. - E
E
is a saturating theorem prover based on a purely equational
view. It combines superposition with rewriting and a large number
of redundancy elimination techniques. Currently, we use E in
automatic mode as a single strategy in E-SETHEO. -
DCTP
DCTP
is our latest inference engine. It is a theorem prover based on
the disconnection tableaux calculus, extended with rules for
handling equality. A particular strenght of DCTP is the ability
to find models for a rather large class of satisfiable clause
sets.
- eground and
SEMPROP
The grounding procedure eground
and the (extended) propositional prover SEMPROP
together form a decision
procedure for the class of CNF problems with a finite Herbrand
universe. eground transforms such problems into
(hopefully small) propositional problems, using constraint-based
techniques, clause splitting, and simlification to handle even
problems that are impossible to tackle with naive grounding
approaches. SEMPROP is then used to decide the resulting
problem. If you are interested in this technique, there also is a
stand-alone system based on the same concept: GrAnDe.
- Complex strategies
In addition to
"pure" strategies based on a single calculus or idea, E-SETHEO
also uses complex strategies, where different provers cooperate
to solve the problem. Most of them are either based on a pipeline
of provers, where one system is used as a preprocessor to
simplify the problem for another system, or on lemma exchange,
where the problem is modifed by the addition of intermediate
results from other provers.
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