|
|
|
This slide
demonstrates the inner workings of the inferencing kernel. The mechanism used
is ‘resolution based inferencing’ also called ‘backward reasoning’.
|
|
I repeat the
database here:
|
|
Rules:
|
|
child(X, Y),
child(Y, Z) :> grandparent(Z, X).
|
|
grandparent(Z,
X), gender(Z, female) :> grandmother(Z, X).
|
|
Facts:
|
|
child(christine,
elza).
|
|
child(wim,
christine).
|
|
sexe(elza,
female).
|
|
The query is:
grandmother(Z,X). The grandmother rule says that somebody is a grandmother
when the person is a grandparent and his gender is female. We now have to
find somebody who is a grandparent with gender female. Two new nodes are
drawn in the search tree:
|
|
grandparent(Z,
X) and gender(Z, female).
|
|
Now some Z is a
grandparent when (a certain) X is a child of (a certain Y) and Y is a child
of Z. Two nodes are added again: child(X, Y) and child(Y, Z).
|
|
Now no more
rules can be applied. But the triple child(X,Y) can match with two facts.
Lets first substitute X by christine and Y by elza to get: child(christine,
elza). In the figure we see now that the node child(Y,Z) becomes: child(elza,
Z). This means we have to find the parent Z of elza; but such fact is not in
the database and therefore a cross is drawn over this goal. So the
substitution that was done (X by christine and Y by elza) was no good. A
backtrack must be done and another alternative has to be tried. Now we
substitute X by wim and Y by christine.
The other child node no becomes:
|
|
child(christine,
Z) and we see that now Z can be susbtituted by elza and the node: gender(Z,
female) now becomes gender(elza, female)
and this is confirmed by a fact in the database. So now we have found
the solution: grandmother(elza, wim).
|
|
The system will
still try to find other solutions but none are found and inferencing
terminates.
|