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.