Third edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2023 is now available (including the full text).

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.

1: Procedure Unify(t1,t2)
2:           Inputs
3:                     t1,t2: atoms Output
4:                     most general unifier of t1 and t2 if it exists or ⊥ otherwise
5:           Local
6:                     E: a set of equality statements
7:                     S: substitution
8:           E ←{t1=t2}
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(x1,...,xn) and y is f(y1,...,yn)) then
20:                                         E←E∪{x1=y1,...,xn=yn}
21:                               else
22:                                         return ⊥
23:           return S
Figure 12.5: Unification algorithm for Datalog

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.