< programming > The generalisation of pattern matching that is the logic programming equivalent of instantiation in logic . When two term s are to be unified, they are compared. 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 recursive ly and the unification succeeds if all the sub-terms unify.
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 ", other unifiers simply add extra bindings for sub-terms which are variables in the original terms.
(1995-12-14)