1.4 Unification

The deduction process involves matching terms in the goal against terms in head of the rule, and terms in the body of the rule against other terms, either in the head of other rules or against facts. The matching process used is termed unification.

Briefly, it works as follows:

Assume the following Prolog program, with four facts and one rule.

male(phil).  
 
female(liz).  
 
parent(phil, chas).  
parent(liz, chas).  
 
mother(M,C):-  
 female(M),  
 parent(M,C).

The goal:

?-mother(liz,chas).

is evaluated like this:

[trace]  ?- mother(liz,chas).  
   Call: (7) mother(liz, chas) ? creep  
   Call: (8) female(liz) ? creep  
   Exit: (8) female(liz) ? creep  
   Call: (8) parent(liz, chas) ? creep  
   Exit: (8) parent(liz, chas) ? creep  
   Exit: (7) mother(liz, chas) ? creep  
 
Yes

In this case the terms in the consequent of the rule matched immediately against facts in the database. Let’s add the following fact and rules to those given above

male(harry).  
 
parent(chas,harry).  
 
grandmother(GM, C):-  
 mother(GM, P),  
 parent(P, C).

The goal grandmother(liz,harry) evaluates as follows:

[trace]  ?-  grandmother(liz,harry).  
   Call: (7) grandmother(liz, harry) ? creep  
   Call: (8) mother(liz, _G329) ? creep  
   Call: (9) female(liz) ? creep  
   Exit: (9) female(liz) ? creep  
   Call: (9) parent(liz, _G329) ? creep  
   Exit: (9) parent(liz, chas) ? creep  
   Exit: (8) mother(liz, chas) ? creep  
   Call: (8) parent(chas, harry) ? creep  
   Exit: (8) parent(chas, harry) ? creep  
   Exit: (7) grandmother(liz, harry) ? creep  
 
Yes

As before, Prolog first tries to prove the leftmost term in the antecedent, but this requires that it search further, since mother(liz,_G329) is not a fact. Only when it has successfully concluded this subproof (via female/1 and parent/2) does it continue to attempt the second clause in the definition of grandmother/2.3

Note that this version of Prolog (like most), renames the variables you supply it with. In this case C has become _G329. This is to avoid accidental clashes of variable-names. Note also that when GM unifies with the constant liz, Prolog only uses the constant in its subsequent search.