In contrast to the saturation-based procedure, which we gave for propositional
resolution, we will discuss now a strategy which allows goal directed generation of resolvents.
We will see later, namely in the case of Horn clauses, that this linear strategy, is the basis
for the interpretation of logic programs.
Given a set of clauses and a clause in . A
linear deduction of top clause is a
sequence , where is a resolvent of and with .
If the sequence is called a linear refutation.
The following is an example for a linear deduction. The clause set is
and together with the goal , we get the following
refutation, where clauses from are given by the respective
, (4),, (2), ,
(1), , (6), ,
the same refutation can be given more naturally be the following
The following theorem states correctness and completeness of linear
resolution. Note that completeness only states that there exists a
linear refutation, there is no guaranty that every clause in the
sequence really is necessary to derive the empty clause.