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

From Wikibooks, open books for an open world
< Logic for Computer Scientists‎ | Predicate Logic‎ | Strategies for Resolution
Jump to: navigation, search

Linear Resolution[edit]

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 S and a clause C_0 in S. A linear deduction of top clause C_0 is a sequence C_0, C_1, \cdots , C_n , where \forall 1\leq i \leq n C_i is a resolvent of C_i and B with B \in S \cup \{C_j \mid j<i \} . If C_n = \square the sequence is called a linear refutation.

Definition 25[edit]

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

\begin{matrix}
symptom(s)  & (1) \\
 
cause(c_1)\lor  cause(c_2) \lor \lnot symptom(s) & (2) \\
 
treatment(t_0)\lor  \lnot cause(c_1) &(3) \\

treatment(t_1)\lor \lnot  cause(c_1) & (4) \\
 
treatment(t_0) \lor \lnot  cause(c_2)&(5) \\
 
treatment(t_2) \lor \lnot cause(c_2)& (6) \\
\end{matrix}


and together with the goal \lnot treatment(x), we get the following refutation, where clauses from S are given by the respective numbers: \lnot treatment(X), (4), \lnot cause(c_1), (2), cause(c_2) \lor \lnot symptom(s), (1), cause(c_2), (6), treatment(t_2), \square

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.



Linearresolution1.png

Theorem 9[edit]

Linear resolution is complete and correct. Example:


Linearresolution2.png