Unification with a list of terms

Question

The problem: we have a list of terms $[t_1, ..., t_n]$ , and a term $t$, and we want to find which of the terms in the list can be unified with $t$. Obviously we can iterate through the list and check one-by-one whether $t_i$ unifies with $t$, but what better (i.e. faster) approaches exist? Assume we can store the list however we want.

I'm particularly interested in approaches that extend well to unification modulo a theory, but assume the empty theory to start.

This must be a basic question but I can't find good references, so any references are much appreciated.

Answer 1

Prolog compilers already do this. Imagine if you had the program:

p(t1) :- body_1.
p(t2) :- body_2.
% ...
p(tn) :- body_n.

and you issued the query p(t).

There is a lot of literature on this topic, and I don't know if there is a recent review which covers it all. You could start with:

Colomb, J. Enhancing Unification in Prolog through Clause Indexing, J. Logic Programming, 1991:10:23-44.