Discrete Mathematics Resolution Principle.

Question

I am having a problem in understanding this following excerpt from Discrete Mathematics Book.

The Resolution Principle : Given a set S of clauses, a (resolution) deduction of C from S is a finite sequence C₁, C₂, ... , C_k of clauses such that each C_i either is a clause in S or a resolvent of clauses preceding C and C_k = C.

My questions

1. What does this theorem states ?
2. What is meant by the line "each C_i either is a clause in S or a resolvent of clauses preceding C and C_k = C" ?

Answer 1

Let me describe the situation on an example. Consider e.g. a formula

$$(\neg A\ \vee\ \neg B\ \vee\ C)\ \wedge A\ \wedge\ B\ \wedge \ \neg C, $$

call it $\varphi$. Now in this situation you have $S=\{(\neg A \vee \neg B \vee C),A,B,\neg C\}$.

I claim that $\varphi$ is a contradiction. In order to do that I can write the following proof in your system.

$C_1:=(\neg A \vee \neg B \vee C)$ member of $S$

$C_2:=A$ member of $S$

$C_3:=(\neg B\vee C)$ resolution to lines 1,2

$C_4:=B$ member of $S$

$C_5:=C$ resolution to lines 3,4.

This is a proof of $C$ from $S$. Notice that you can write a one line proof of $\neg C$ also. So you have infered both an atom and its negation. Thus $S$ is not satisfiable, and the same holds for $\varphi$.

Comments: formula is called literal, if it is either atomic or a negation of an atomic formula. It is called a clause if it is a finite disjunction of literals. Thus in the example $S$ is a set of clauses ($A,B,C$ are atomic). Now on each line of the proof you can write a clause which is either a member or S or a resolvent of previous clauses. In the example $C_1,C_2,C_4$ are members of $S$. Whereas e.g. $C_3$ is a resolvent of $C_1$ and $C_2$, meaning it has been derived from $C_1$ and $C_2$ using the resulution rule, which has the following general form:

$$\frac{(l_1\vee\dots\vee l_{i-1}\vee A\vee l_{i+1}\dots\vee l_m )\,\,\,\, (s_1\vee\dots\vee s_{j-1}\vee \neg A\vee s_{j+1}\dots\vee s_n) }{l_1\vee\dots\vee l_{i-1}\vee l_{i+1}\dots\vee l_m \vee s_1\vee\dots\vee s_{i-1}\vee s_{i+1}\dots\vee s_n },$$ where all $l_i$ and $s_i$ are literals. The case of inference of $C_3$:

$$\frac{A \,\,\,\, (\neg A \vee \neg B \vee C)}{\neg B\vee C}$$

Intuition: You read each line $n$ as a proof of the clause $C_n$ from $S$. In particular, in order to prove $C_n$ you needed to prove $C_i$ for $i<n$ before (this explains the 'or is a resolution of preceeding clauses', you first prove some $C_i,C_j$ and then you apply resolution to obtain $C_k$ on some line $k>i,j$). A key property behind: if $v$ is a valuation satisfying every clause in $S$ then $v$ also satisfies every $C$, which you can prove this way (every $C_i$ on every proof sequence will be true under $v$);Indeed, if $C\in S$ a $v$ satisfies $S$ it obviously satisfy $C$, and it is easy to see that if $v$ satisfies the clauses which are premises of the resolution rule, it also satisfy its conclusion! This validity preservation is what you want this machinery to fulfil: this explains why you can write $C\in S$ on an arbitrary line in the proof. Finally the $C_k=C$ means simply that in the last step of the proof (the step $k$), in which you proved the formula $C_k$, you have actually proven $C$.