Unification

A 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:

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

FOLDOC definition.

This page is linked from: Alan Bundy Dispatch LIFE TXL