Logic for Computer Scientists/Predicate Logic/Strategies for Resolution/Linear Resolution

From Wikibooks, open books for an open world
Jump to navigation Jump to search

Linear Resolution[edit | edit source]

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.

Definition 25[edit | edit source]

The following is an example for a linear deduction. The clause set is given by:


and together with the goal , we get the following refutation, where clauses from are given by the respective numbers: , (4),, (2), , (1), , (6), ,

the same refutation can be given more naturally be the following picture: 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.



Theorem 9[edit | edit source]

Linear resolution is complete and correct. Example: