Engineering a High-Performance Equational Theorem Prover

First order predicate logic is at the core of many applications in
mathematics, AI, and verification. It is one of the most studied
logics in computer science, offering an attractive compromise between
expressibility and automatability. However, automatic reasoning in
first order logic has to deal with infinite search spaces. Typically,
the large number of possible deductions lead to an explosion of the
search space, i.e. the size of the search state grows exponentially
with the number of inferences drawn, or, alternatively, the maximum
proof length.

The last years have seen the convergence of several research streams
in resolution-based theorem proving and rewriting, resulting in a the
"superposition calculus", a refutationally complete calculus for first
order clausal logic with equality. Its model-based completeness proof
yields a very powerful abstract notion of redundancy that allows us to
discard large parts of the search space. However, to translate this
abstract calculus into a concrete procedure is far from trivial.

In this talk we will describe some of the features of the
superposition-based theorem prover E. We will show how efficiently
implementable, concrete redundancy elimination criteria have been
developed, and how crucial the role of efficient data structures and
good search heuristics is.

A preliminary overview on E can be obtained at http://www.eprover.org.