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.