# 13.4.3 Unification

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 $\bot$ if they do not unify.

The unification algorithm is given in Figure 13.3. $E$ is a set of equality statements implying the unification, and $S$ is a set of equalities of the correct form of a substitution. In this algorithm, if $\alpha/\beta$ is in the substitution $S$, then, by construction, $\alpha$ is a variable that does not appear elsewhere in $S$ or in $E$. In line 20, $\alpha$ and $\beta$ must have the same predicate and the same number of arguments; otherwise the unification fails.

###### Example 13.22.

Suppose you want to unify $p(X,Y,Y)$ with $p(a,Z,b)$. Initially $E$ is $\{p(X,Y,Y)=p(a,Z,b)\}$. The first time through the while loop, $E$ becomes $\{X=a,Y=Z,Y=b\}$. Suppose $X=a$ is selected next. Then $S$ becomes $\{X/a\}$ and $E$ becomes $\{Y=Z,Y=b\}$. Suppose $Y=Z$ is selected. Then $Y$ is replaced by $Z$ in $S$ and $E$. $S$ becomes $\{X/a,Y/Z\}$ and $E$ becomes $\{Z=b\}$. Finally $Z=b$ is selected, $Z$ is replaced by $b$, $S$ becomes $\{X/a,Y/b,Z/b\}$, and $E$ becomes empty. The substitution $\{X/a,Y/b,Z/b\}$ is returned as an MGU.

Consider unifying $p(a,Y,Y)$ with $p(Z,Z,b)$. $E$ starts off as $\{p(a,Y,Y)=p(Z,Z,b)\}$. In the next step, $E$ becomes $\{a=Z,Y=Z,Y=b\}$. Then $Z$ is replaced by $a$ in $E$, and $E$ becomes $\{Y=a,Y=b\}$. Then $Y$ is replaced by $a$ in $E$, and $E$ becomes $\{a=b\}$, and then $\bot$ is returned indicating that there is no unifier.