In computer science, term indexing is the task of creating an index of terms and clauses in a collection.
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 of terms (clauses) and a query term (clause), find in some/all terms related to 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 . Here is a list of retrieval conditions frequently used in provers:
- term is unifiable with term, i.e., there exists a substitution, such that =
- term is an instance of, i.e., there exists a substitution, such that =
- term is a generalisation of, i.e., there exists a substitution, such that =
- clause subsumes clause, i.e., there exists a substitution, such that is a subset/submultiset of
- clause is subsumed by, i.e., there exists a substitution, such that is a subset/submultiset of
More often than not, we are actually interested in finding the appropriate substitutions explicitly, together with the retrieved terms, 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, when the retrieval condition is tested on every term from, 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.
Read more about Term Indexing: Classic Indexing Techniques, Modern Indexing Techniques, Further Reading
Famous quotes containing the word term:
“A radical is one of whom people say “He goes too far.” A conservative, on the other hand, is one who “doesn’t go far enough.” Then there is the reactionary, “one who doesn’t go at all.” All these terms are more or less objectionable, wherefore we have coined the term “progressive.” I should say that a progressive is one who insists upon recognizing new facts as they present themselves—one who adjusts legislation to these new facts.”
—Woodrow Wilson (1856–1924)