1. Constants and variables are terms.
  2. A compound term consists of a functor characterized by its name and arity, or number of arguments. Each argument is a term. Syntactically a compound term has the form f(t1, ...., tn) where f is the functor's name and t1, ... , tn are its arguments.
Given two terms S and T, they unify if there exists a substitution s such that Ss =Ts, where Ss (resp.) Ts denotes the result of applying s to S (resp. T). The most general unifer of two terms S and T is a substitution m such that
  1. Sm = Tm
  2. If s is a substitution such that Ss=Ts then there is a substitution t such that s = m.t

The following algorithm produces the mgu if it exists.

The Unification Algorithm

Two terms T1 and T2 to be unified
s, the mgu of T1 and T2 or failure
Initialize s to be empty
Initialize the stack to contain the equation T1 = T2
and failure to be false

while stack not empty and failure equals false do

pop X = Y from the stack

           X is a variable that does not occur in Y:
              substitute Y for X in the stack and in t
              add X = Y to t.

          Y is a variable that does not occur in X:
              substitute X for Y in the stack and in t
              add Y = X to t

	X and Y are identical constants or variables:
           X is f(X1, ..., Xn) and Y is f(Y1, ... , Yn)
                for some functor f and n > 1:
                push Xi=Yi, i =1, ...n, on the stack
                set failure to true.
if failure equals true , then output failure
else output t.

Note that this algorithm uses an occurs check so that it will not unify X and f(X).

Return to UG AI home page

Last Changed: 14 August 1995