# Unification with a list of terms

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.

p(t1) :- body_1.

and you issued the query p(t).