Term indexing

In computer science, a term index is a data structure to facilitate fast lookup of terms and clauses in a logic program,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 ${\displaystyle S}$ of terms (clauses) and a query term (clause) ${\displaystyle q}$, find in ${\displaystyle S}$ some/all terms ${\displaystyle t}$ related to ${\displaystyle 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 ${\displaystyle t}$. Here is a list of retrieval conditions frequently used in provers:

...
Wikipedia