The power of a deduction system is not only determined by the problems it is able to solve, but also by the speed it solves these problems. One way to speed up a theorem prover is to improve the maintenance of data referred to by the deduction system. Different methods for term retrieval in deduction systems have been introduced in literature. At the moment ACID provides different versions of path and discrimination tree indexing. It consists of a set of data structures which provide fast access to special entries of a term-base.
Indexing is employed in different tasks in automated reasoning.
In order to find resolution partners for a given literal, for example, a theorem prover has to search for literals which unify with a given literal. The retrieval of rewrite rules and demodulators can be accelerated by indexing as well. Available files for downloading You can get the documentation and the software by browsing the ACID directory on our ftp server . Alternatively here is a list of the files for individual downloading. Sicstus.tar.gz - the substitution tree indexing package for Sicstus Prolog in gzip'ed tar format.