Section 1.5 Logic Programming
77
which is just an application of modus ponens. Therefore Prolog’s rule of inference
includes modus ponens as a special case.
In applying the resolution rule, variables are considered to “match” any
constant symbol. (This is the repeated application of universal instantiation.) In
any resulting new clause, the variables are replaced with their associated constants in a consistent manner. Thus in response to the query ?prey(X ), Prolog
searches the database for a rule with the desired predicate Pr(x) as the consequent. It finds
[E( y, x)]′ ~ [A(x)]′ ~ Pr(x)
It then proceeds through the database looking for other clauses that can be resolved with this clause. The first such clause is the fact E(b, fi). These two clauses
resolve into
[A( fi)]′ ~ Pr( fi)
(Note that the constant fi has replaced x everywhere.) Using this new clause, it
can be resolved with the fact A( fi) to conclude Pr( fi). Having reached all conclusions possible from resolution with the fact E(b, fi), Prolog backtracks to search
for another clause to resolve with the rule clause; this time around it would find
E(b, fo).
As a more complex example of resolution, suppose we add the rule
hunted(X ) <= prey(X )
to the database. This rule in symbolic form is
[Pr(x)] S H(x)
or, as a Horn clause,
[Pr(x)]′ ~ H(x)
It resolves with the rule defining prey
[E( y, x)]′ ~ [A(x)]′ ~ Pr(x)
to give the new rule
[E( y, x)]′ ~ [A(x)]′ ~ H(x)
The query
?hunted(X )
will use this new rule to conclude
fish
fox