Term indexing

In computer science, a term index is a data structure to facilitate fast lookup of terms and clauses in a logic program,[1] deductive database, or automated theorem prover.

Many operations in automatic theorem provers require search in huge collections of terms and clauses. Such operations typically fall into the following scheme. Given a collection S of terms (clauses) and a query term (clause) q, find in S some/all terms t related to q according to a certain retrieval condition. Most interesting retrieval conditions are formulated as existence of a substitution that relates in a special way the query and the retrieved objects t. Here is a list of retrieval conditions frequently used in provers:

More often than not, we are actually interested in finding the appropriate substitutions explicitly, together with the retrieved terms t, rather than just in establishing existence of such substitutions.

Very often the sizes of term sets to be searched are large, the retrieval calls are frequent and the retrieval condition test is rather complex. In such situations linear search in S, when the retrieval condition is tested on every term from S, becomes prohibitively costly. To overcome this problem, special data structures, called indexes, are designed in order to support fast retrieval. Such data structures, together with the accompanying algorithms for index maintenance and retrieval, are called term indexing techniques.

Classic indexing techniques

Modern indexing techniques

References

  1. Colomb, Robert M. (1991). "Enhancing unification in PROLOG through clause indexing". The Journal of Logic Programming 10: 23. doi:10.1016/0743-1066(91)90004-9.

Further reading

This article is issued from Wikipedia - version of the Saturday, August 29, 2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.