If we are to prove a given goal g
then each R
in the derived rules would have to be g
, and the initial axiom would be of the form
Reading top-down, we see a strategy that starts with the desired
goal in the context, and in each derived rule selects a literal from
among the current goals in the context that is the head of a
Horn-clause, and replaces it with the body of the clause. This is the
famous SLD-resolution, familiar from top-down logic programming (such
as in Prolog).
In the same reading of a proof (from the premisses down to the
conclusion), we are thus able to obtain the two different semantics of
Horn-clauses—forward chaining and backward chaining—as a
direct consequence of the assignment of polarities to the atoms. It
should be no surprise that in the opposite reading of the rules (from
the conclusion to the premisses), we also observe (a dualised form of)
SLD-resolution and hyperresolution. This observation extends (with some
additional work) to first-order Horn-clauses also.
To slightly emphasize an easily missed consequence, we see that forward
and backward reasoning can cohabit in the same general search strategy
by careful assignment of polarity to the atoms. For an illuminating
example, consider the computation of Fibonacci numbers by means of the
following short collection of Horn-clauses.
fib(z, s z).
fib(s z, s z).
fib(s s N, K), ¬fib(s M, I), ¬fib(M,J), ¬add(I,J,K).
add(s M, N, s K), ¬add(M,N,K).