Stephan Schulz: Simple and Efficient Clause Subsumption with Feature
                Vector Indexing 
 
Abstract

We describe _feature vector indexing_, a new, non-perfect indexing
method for clause subsumption. It is suitable for both forward
(i.e., finding a subsuming clause in a set) and backward (finding
all subsumed clauses in a set) subsumption. Moreover, it is easy to
implement, but still yields excellent performance in practice. As an
added benefit, by restricting the selection of features used in the
index, our technique immediately adapts to indexing modulo arbitrary
AC theories with only minor loss of efficiency. Alternatively, the
feature selection can be restricted to result in _set
subsumption_.

Feature vector indexing has been implemented in our equational
theorem prover E, and has enabled us to integrate new simplification
techniques making heavy use of subsumption. We experimentally
compare the performance of the prover for a number of strategies
using feature vector indexing and conventional sequential
subsumption.