A theorem prover's performance in terms of logical inferences per second crucially depends on the speed of its basic retrieval operations, such as finding terms unifiable with some query term, for example. In the literature various indexing methods for term retrieval in deduction systems have been introduced. In this paper we present an indexing method that supports indexing in presence of associative and commutative function symbols.
展开▼
