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 $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 $\mathrm{\forall }1\le i\le n$ $C_i$ is a resolvent of $C_{i-1}$ and $B$ with $B\in S\cup \{C_j\mid j<i\}$ . If $C_n=◻$ the sequence is called a linear refutation.

Definition 25

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

$\begin{array}{cc}symptom(s)& (1)\\ cause(c_1)\vee cause(c_2)\vee \mathrm{\neg }symptom(s)& (2)\\ treatment(t_0)\vee \mathrm{\neg }cause(c_1)& (3)\\ treatment(t_1)\vee \mathrm{\neg }cause(c_1)& (4)\\ treatment(t_0)\vee \mathrm{\neg }cause(c_2)& (5)\\ treatment(t_2)\vee \mathrm{\neg }cause(c_2)& (6)\end{array}$

and together with the goal $\mathrm{\neg }treatment(x)$, we get the following refutation, where clauses from $S$ are given by the respective numbers: $\mathrm{\neg }treatment(X)$, (4),$\mathrm{\neg }cause(c_1)$, (2), $cause(c_2)\vee \mathrm{\neg }symptom(s)$, (1), $cause(c_2)$, (6), $treatment(t_2)$,$◻$

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

Linear resolution is complete and correct. Example: