Project "Contraintes" Prolog Web Pages: Unification
One of the interesting outcomes of the standardization process was
the realization that not everybody agreed on what is meant by unification.
The ISO standard therefor provides a (nondeterministic) algorithm, the
``Herbrand Algorithm'' that computes the most general unifier (MGU) of a set of equations.
The standard does not specify how the algorithm is to be implemented.
It requires that (at least in the case of
unify_with_occurs_check/2
the result shall be as specified by the Herbrand algorithm.
The Herbrand Algorithm for an MGU
Given a set of equations of the form t_{1} = t_{2}
apply in any order one of the following nonexclusive steps:
 If there is an equation of the form:
 f=g where f and g are different
atomic terms, or
 f=g where f is an atomic term and g is
a compound term, or f is a compound term and g is an atomic term, or
 f(...) = g(...) where f and g are different functors, or
 f(a_{1}, a_{2}, ..., a_{N}) =
g(b_{1}, b_{2}, ..., b_{M})
where N and M are different.
then exit with failure (not unifiable).
 If there is an equation of the form X = X, X being a
variable, then remove it.
 If there is an equation of the form c = c, c being a
atomic term, then remove it.
 If there is an equation of the form f(a_{1}, a_{2}, ..., a_{N}) =
f(b_{1}, b_{2}, ..., b_{N})
then replace it by the set of equations a_{i} = b_{i}.
 If there is an equation of the form t = X, X being a
variable and t a nonvariable term, then replace it by the equation
X = t,
 If there is an equation of the form X = t where:
 X is a variable and t a term in which the
variable does not occur, and
 the variable X occurs in some other equation,
then substitute in all other equations every occurrence of the variable X
by the term t.
 If there is an equation of the form X = t such that X
is a variable and t a nonvariable term which contains this variable,
then exit with failure
(not unifiable, positive occurs check.

If no other step is applicable, then exit with success (unifiable).
Example of a positive occurs check
The equation f(X,X,X) = f(Y,g(Y),a) is not unifiable being subject to a positive occurs check. It leads to an attempt to unify Y with
g(Y). This is seen as follows.
 Apply rule 4 to get X = Y, X = g(Y), X = a
 Apply rule 6 to get X = Y, Y = f(Y), Y = a
 Now rule 7 applies to the second equation.
Author: J.P.E. Hodgson
Saint Joseph's University
Philadelphia PA 19131
USA
Last Changed: 20 January 1999