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.
To overcome this problem, special data structures, called indexes, are designed in order to support fast retrieval.
[2] A discrimination tree term index stores its information in a trie data structure.
It distinguishes atomic values and the principal functor of compound terms.
Deep indexing is used when multiple clauses use the same principal functor for some argument.
It recursively uses the same or similar indexing techniques on the arguments of the compound terms.
Trie indexing uses a prefix tree to find applicable clauses.