13.4 Proofs and Substitutions

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

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 ⊥ if they do not unify.

1: procedure Unify(t1,t2)
2:      Inputs
3:          t1,t2: atoms or terms      
4:      Output
5:          most general unifier of t1 and t2 if it exists or ⊥ otherwise
6:      Local
7:          E: a set of equality statements
8:          S: substitution      
9:      E←{t1=t2}
10:      S={}
11:      while E≠{} do
12:          select and remove α=β from E
13:          if β is not identical to α then
14:               if α is a variable then
15:                   replace α with β everywhere in E and S
16:                   S←⁢{α/β}∪S
17:               else if β is a variable then
18:                   replace β with α everywhere in E and S
19:                   S←⁢{β/α}∪S
20:               else if α is p⁢(α1,…,αn) and β is p⁢(β1,…,βn) then
21:                   E←E∪{α1=β1,…,αn=βn}
22:               else
23:                   return ⊥                             
24:      return S
Figure 13.3: Unification algorithm for Datalog

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 α/β is in the substitution S, then, by construction, α is a variable that does not appear elsewhere in S or in E. In line 20, α and β 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 ⊥ is returned indicating that there is no unifier.