Implementation of Saturating Theorem Provers

                     Stephan Schulz

We will describe several aspects of the implementation of a
saturating, superposition-based theorem prover for first-order
logic. We discuss the basic architecture of a prover, and the
organization of the actual proof search via the given-clause
algorithm. Simplification and redundancy elimination are, in practice,
critical, and we describe how these can be integrated into the basic
proof procedure.

Another topic is that of terms and clauses, the most basic data
objects in any prover, and how they can be implemented. We discuss
bottlenecks of naive implementations, as well as the principle and
some examples of indexing techniques to overcome these bottlenecks.
The presentation concludes with a look at the influence of search
heuristics.