foundations of computational agents
The problem of unification is the following: given two atoms or terms, determine whether they unify, and, if they do, return a unifier of them. The unification algorithm finds a most general unifier (MGU) of two atoms or returns if they do not unify.
The unification algorithm is given in Figure 13.3. is a set of equality statements implying the unification, and is a set of equalities of the correct form of a substitution. In this algorithm, if is in the substitution , then, by construction, is a variable that does not appear elsewhere in or in . In line 20, and must have the same predicate and the same number of arguments; otherwise the unification fails.
Suppose you want to unify with . Initially is . The first time through the while loop, becomes . Suppose is selected next. Then becomes and becomes . Suppose is selected. Then is replaced by in and . becomes and becomes . Finally is selected, is replaced by , becomes , and becomes empty. The substitution is returned as an MGU.
Consider unifying with . starts off as . In the next step, becomes . Then is replaced by in , and becomes . Then is replaced by in , and becomes , and then is returned indicating that there is no unifier.