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.


1 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.