E 0.7
S. Schulz
Institut für Informatik, Technische Universität
München, Germany
schulz@informatik.tu-muenchen.de
Architecture
E 0.7[Sch99] is a purely equational
theorem prover. The calculus used by E combines superposition (with
selection of negative literals) and rewriting. For the special case
that only unit clauses are present, it degenerates into unfailing
completion, for the Horn case, E can simulate various positive
unit strategies. No special rules for non-equational literals have
been implemented, i.e., resolution is simulated via paramodulation and
equality resolution.
Proof search in E is controlled by a literal selection strategy and an
evaluation heuristic. A variety of selection strategies (including
e.g., no selection, or select all negative literals)
is available. Evaluation heuristics can be constructed on the fly by
combining various parameterized primitive evaluation functions. A
simple automatic mode can select strategy, term ordering, and
heuristic based on simple problem characteristics.
New features since last year include a wider variety of literal
selection strategies, and an improved automatic mode that now also
switches between two different Knuth-Bendix orderings. A proof checker
is now available as well.
Implementation
E is implemented in ANSI C, using the GNU C compiler. The most unique
feature of the implementation is the maximally shared term
representation. This includes parallel rewriting for all instances of
a particular subterm. A second important feature is the use of
perfect discrimination trees with age and size constraints
for rewriting and unit-subsumption.
The program has been successfully installed under SunOS 4.3.x,
Solaris 2.x, HP-UX B 10.20, and various versions of
Linux. Sources are available freely from:
http://wwwjessen.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
Expected Competition Performance
As in the last year, we expect E to perform pretty well in all
categories it participates in, with particularly strong showing for
Horn problems. We have spend very little effort on the performance for
unit problems, however, and it is unlikely that we can come close to
Waldmeister's performance in this category.
E's auto mode is optimized for performance on the complete TPTP
2.3.0. The optimization is based on a fairly large number of test runs
and consists of the selection of one of about 50 different strategies
for each problem.
References
- Sch99
- Schulz S. (1999),
System Abstract: E 0.3,
Ganzinger H.,
Proceedings of the 16th International Conference on Automated
Deduction
(Trento, Italy),
Lecture Notes in Artificial Intelligence,
Springer-Verlag, pp.297--391