Fingerprint Indexing for Paramodulation and Rewriting
                      (Extended Version)
                        Stephan Schulz

Indexing is critical for the performance of automated first-order
theorem provers. We introduce \emph{fingerprint indexing}, a
non-perfect indexing technique that is based on short, constant
length vectors of samples of term positions (``fingerprints'')
organized in a trie. Fingerprint indexing supports both matching and
unification as retrieval relations. The algorithms are simple, the
indices are small, and performance is very good in practice.

We have implemented fingerprint indexing in the equational theorem
prover E, where it is used for backwards rewriting and
superposition. We demonstrate the performance of the index both in
relative and absolute terms using large-scale profiling.