Perfect discrimination graphs: Indexing terms with integer exponents

Abstract

Perfect discrimination trees [12] are used by many efficient resolution and superposition-based theorem provers (e.g. E-prover [17], Waldmeister [10], Logic Reasoner, ...) in order to efficiently implement rewriting and unit subsumption. We extend this indexing technique to handle a class of terms with integer exponents (or I-terms), a schematisation language allowing to capture sequences of iterated patterns [8]. We provide an algorithm to construct the so called perfect discrimination graphs from I-terms and to retrieve indexed I-terms from their instances. Our research is essentially motivated (but not restricted to) by some approaches to inductive proofs, for which termination of the proof procedure is capital. © 2010 Springer-Verlag.