Abstraction Tree Indexing for Terms

An indexing technique for first-order predicate logic terms and literals is proposed. It exploits the lattice structure of terms, generated by the usual instance relation, to provide for a given "query term" fast access to all T-unifiable terms, T-instances (backward subsumption) and T-generalized terms (forward subsumption) where T is any finitary unification theory. In the best case one single unification or matching operation respectively is sufficient to access a large number of unifiable terms or instances at once