On the Evaluation of Indexing Techniques for Theorem Proving
Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Андрей Воронков · 2001
This article is structured as follows. Section 2 discusses some design decisions taken after numerous discussions of the authors. Section 3 gives benchmarks for term retrieval and index maintenance for the problem of retrieval of generalizations (matching a query term by index terms), generated by running our provers Vampire [20], Fiesta [15] and Waldmeister [9] (three rather dierent, we believe quite representative, state-of-the-art provers) on a selection of carefully chosen problems from dierent domains of the TPTP library [25].