The following algorithm produces the mgu if it exists.
while stack not empty and failure equals false do
pop X = Y from the stack
case 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: continue 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 otherwise: set failure to true.if failure equals true , then output failure
Note that this algorithm uses an occurs check so that it will not unify X and f(X).
Last Changed: 14 August 1995