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:

to unify two terms must be of the same arity - that is, they must take the same number of arguments.

if this condition is satisfied, then unification reduces ultimately to a matching of the basic terms in a compound expression. Basic terms unify as follows:

1. identical constants unify (e.g. chas and chas).
2. a constant and a variable unify (e.g. chas and X) - and as a side-effect, the variable becomes instantiated to the value of the constant. (So from the point of unification on, the variable ceases to be a variable.)
3. two variables unify. (X and Y will become the same variable).
   

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:

| ?- mother(liz,chas).
       1     1 Call: mother(liz,chas) ?
       2     2 Call: female(liz) ?
       2     2 Exit: female(liz) ?
       3     2 Call: parent(liz,chas) ?
       3     2 Exit: parent(liz,chas) ?
       1     1 Exit: mother(liz,chas) ?

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 rule 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:

| ?- grandmother(liz,harry) .
       1     1 Call: grandmother(liz,harry) ?
       2     2 Call: mother(liz,_732) ?
       3     3 Call: female(liz) ?
       3     3 Exit: female(liz) ?
       4     3 Call: parent(liz,_732) ?
       4     3 Exit: parent(liz,chas) ?
       2     2 Exit: mother(liz,chas) ?
       5     2 Call: parent(chas,harry) ?
?      5     2 Exit: parent(chas,harry) ?
?      1     1 Exit: grandmother(liz,harry) ?

yes

As before, Prolog first tries to prove the leftmost term in the antecedent, but this requires that it search further, since mother(liz,_732) 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.[1]

Note that this version of Prolog (like most), renames the variables you supply it with. In this case C has become _732. 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.

[1] Note the standard conventional way of citing a Prolog predicate in the form predicate_name/arity.