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
- Constants and variables are terms.
- 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.
- Sm = Tm
- 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).
UG AI home page
Last Changed: 14 August 1995