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

Linear Resolution 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 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. Image:linearresolution1.png Theorem 9 Linear resolution is complete and correct. Example: Image:linearresolution2.png