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.
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
- Single strategy, aggressive contextual unit cutting, 75
AC-compatible features, permuted feature vectors:
- E 0.8 automatic mode, 75 AC-compatible features, permuted feature
Additional test runs
- E 0.8 automatic mode, permuted AC-compatible features: