The E Equational Theorem Prover

Feature Vector Indexing

Feature vector indexing is a new technique for speeding up various variants of forward and backward clause subsumption, important redundacy elimination techniques for first-order theorem provers. It is described in detail in my paper Simple and Efficient Clause Subsumption with Feature Vector Indexing. This web site primarily presents more detailed experimental results.

Feature vector indexing works by representing a clause as a feature vector using a number of subsumption compatible clause features. A potential subsumer can only subsume another clause if its feature vector is smaller than or equal (in a suitable ordering) than the one of the (potentially) subsumed clause. By organizing feature vectors into a trie, we can quickly filter out a small number of suitable candidates for subsumption (in either direction) from a larger set of clauses.

Experimental Results

Note: You can download and install the current version of E and use the development_tools/eauswert.awk script to summarize the results.

We used all 5180 clause normal form problems from TPTP 2.5.1, in expanded TPTP format, without equality axiom, but otherwise unchanged. All test runs were performed on a cluster of 300MHz SUN Ultra-60 workstations with a time limit of 300 seconds (or equivalent configurations). The memory limit was 192 MB.

Results discussed in the paper

Additional test runs

Impressum