UnificationA term generalizing that of pattern-matching that is the logic programming equivalent of instantiation in logic.
Citing from FOLDOC (slightly reformatted, see below):
When two terms are to be unified, they are compared:
The result of unification is either failure or success with a set of variable bindings, known as a "unifier". There may be many such unifiers for any pair of terms but there will be at most one "Most General Unifier" (MGU), other unifiers simply add extra bindings for sub-terms which are variables in the original terms.
- if they are both constants then the result of unification is success if they are equal else failure;
- if one is a variable then it is bound to the other, which may be any term (which satisfies an "occurs check"), and the unification succeeds;
- if both terms are structures then each pair of sub-terms is unified recursively and the unification succeeds if all the sub-terms unify.