E/EP 1.4pre

Stephan Schulz
Technische Universität München, Germany

Architecture

E 1.4pre [Sch2002,Sch2004] is described in this section. E is a purely equational theorem prover for full first-order logic with equality. It consists of an (optional) clausifier for pre-processing full first-order formulae into clausal from, and a saturation algorithm implementing an instance of the superposition calculus with negative literal selection and a number of redundancy elimination techniques. E is based on the DISCOUNT-loop variant of the given-clause algorithm, i.e., a strict separation of active and passive facts. No special rules for non-equational literals have been implemented. Resolution is effectively simulated by paramodulation and equality resolution.

EP 1.4pre is just a combination of E 1.4pre in verbose mode and a proof analysis tool extracting the used inference steps. For the LTB division, a control program uses a SInE-like analysis to extract reduced axiomatizations that are handed to several instances of E.

Strategies

Proof search in E is primarily controlled by a literal selection strategy, a clause evaluation heuristic, and a simplification ordering. The prover supports a large number of pre-programmed literal selection strategies. Clause evaluation heuristics can be constructed on the fly by combining various parametrized primitive evaluation functions, or can be selected from a set of predefined heuristics. Clause evaluation heuristics are based on symbol-counting, but also take other clause properties into account. In particular, the search can prefer clauses from the set of support, or containing many symbols also present in the goal. Supported term orderings are several parametrized instances of Knuth-Bendix-Ordering (KBO) and Lexicographic Path Ordering (LPO).

The automatic mode is based on a static partition of the set of all clausal problems based on a number of simple features (number of clauses, maximal symbol arity, presence of equality, presence of non-unit and non-Horn clauses,...). Each class of clauses is automatically assigned a heuristic that performs well on problems from this class in test runs. About 100 different strategies have been evaluated on all untyped first-order problems from TPTP 4.1.0.

Implementation

E is build around perfectly shared terms, i.e. each distinct term is only represented once in a term bank. The whole set of terms thus consists of a number of interconnected directed acyclic graphs. Term memory is managed by a simple mark-and-sweep garbage collector. Unconditional (forward) rewriting using unit clauses is implemented using perfect discrimination trees with size and age constraints. Whenever a possible simplification is detected, it is added as a rewrite link in the term bank. As a result, not only terms, but also rewrite steps are shared. Subsumption and contextual literal cutting (also known as subsumption resolution) is supported using feature vector indexing [Sch2004b]. Superposition and backward rewriting use fingerprint indexing, a new technique combining ideas from feature vector indexing and path indexing. Finally, LPO and KBO are implemented using the elegant and efficient algorithms developed by Bernd Löchner in [Loe2006, Loe06b]. The prover and additional information are available at the following address:

    http://www.eprover.org

Expected Competition Performance

E 1.4pre is relatively little changed from last years entry. The system is expected to perform well in most proof classes, but will at best complement top systems in the disproof classes.

References

Sch2002: Schulz S. (2002), E: A Brainiac Theorem Prover, Journal of AI Communications 15(2/3), 111-126, IOS Press
Sch2004: Schulz S. (2004), System Abstract: E 0.81, Proceedings of the 3rd IJCAR (Cork, Ireland), Lecture Notes in Artificial Intelligence, Springer-Verlag
Sch2004b: Schulz S. (2004), Simple and Efficient Clause Subsumption with Feature Vector Indexing, Proceedings of the IJCAR-2004 Workshop on Empirically Successful First-Order Theorem Proving, (Cork, Ireland)
Loe2006: Löchner B. (2004), Things to know when implementing LPO, International Journal on Artificial Intelligence Tools, 15(1), pp.53–80, 2006.
Loe2006b: Löchner B. (2006), Things to Know When Implementing KBO, Journal of Automated Reasoning 36(4), pp.289-310.