ESFOR 2004 Preliminary Version 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. Key words: automated theorem proving, saturation, subsumption, indexing 1 Introduction First-order theorem proving is one of the core areas of automated deduction. In this field, saturating theorem provers have, in the last few years, developed a significant lead compared to systems based on other paradigms, such as top-down reasoning or instance-based methods