#### 12.4.2.1 Unification

The preceding algorithms assumed that we could find the **most general unifier** of two
atoms. The problem of
**unification** is the following: given two atoms,
determine if they unify, and, if they do, return
an MGU of them.

**Procedure**Unify(

*t*)

_{1},t_{2}2:

**Inputs**

3:

*t*: atoms

_{1},t_{2}**Output**

4: most general unifier of

*t*and

_{1}*t*if it exists or

_{2}*⊥*otherwise

5:

**Local**

6:

*E*: a set of equality statements

7:

*S*: substitution

8:

*E ←{t*

_{1}=t_{2}}9:

*S={}*

10:

**while**(

*E≠{}*)

11: select and remove

*x=y*from

*E*

12:

**if**(

*y*is not identical to

*x*)

**then**

13:

**if**(

*x*is a variable)

**then**

14: replace

*x*with

*y*everywhere in

*E*and

*S*

15:

*S←{x/y}∪S*

16:

**else if**(

*y*is a variable)

**then**

17: replace

*y*with

*x*everywhere in

*E*and

*S*

18:

*S←{y/x}∪S*

19:

**else if**(

*x*is

*f(x*and

_{1},...,x_{n})*y*is

*f(y*)

_{1},...,y_{n})**then**

20:

*E←E∪{x*

_{1}=y_{1},...,x_{n}=y_{n}}21:

**else**

22:

**return**

*⊥*

23:

**return**

*S*

The unification algorithm is given in Figure 12.5. *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 *x/y* is in the substitution *S*, then, by
construction, *x* is a variable that does not appear elsewhere in *S* or in
*E*. In line 19, *x* and *y* must
have the same predicate and the same number of arguments; otherwise
the unification fails.

**Example 12.22:**Suppose we 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.