I am a newbie in propositional logic and I am learning by myself. I am reading the book A First Course in Logic : An Introduction to Model Theory, Proof Theory, Computability, and Complexity by Hedman. In this book, it is said that the proof system based on the resolution rule is sound (formula derived using repeatedly the resolution rule are consequence) and complete (any consequence can be derived using repeatedly the resolution rule) for propositional logic with formula in conjunctive normal form. I toyed with some simple examples and found a formula for which a consequence is not derived with the use of the resolution rule. What did I miss?

The example is a formula in conjunctive normal form with two variables $x_1$ and $x_2$. The clauses are $\{ x_1 \}$ and $\{ x_2 \}$. A consequence is $\{ x_1, x_2 \}$ but I cannot see how this can derived with the resolution rule.

The definitions of the book are.

Assignment: let $S = \{ x_1, \dots, x_n \}$ be a set of atomic formulas. An assignment of $S$ is a function $A : S \rightarrow \{ 0, 1 \}$. (Basically, an assignment assign true or false to the atomic formulas.)

The notion of assignment extends to formula. Let $F$ be a formula and $A$ be an assignment. $A(F)$ is the truth value of $F$ when valuated with the assignment. $A$ is said to model $F$ when $A(F) = true$; this denoted $A \vDash F$.

Consequence: Formula $G$ is a consequence of formula $F$ if for every assignment $A$, if $A$ models $F$, then $A$ models $G$ (if $A \vDash F$, then $A \vDash G$). It is denoted $F \vDash G$.

Resolution rule: let $C_1$ and $C_2$ be two clauses. Suppose $x_i\in C_1$ and $\lnot x_i \in C_2$ for some atomic formula $x_i$. The resolvent $R$ is $R = (C_1-\{ x_i \}) \cup (C_2 - \{ \lnot x_i \})$. Then $R$ is derived from $C_1$ and $C_2$. It is denoted $\{ C_1, C_2 \} \vdash R$.


Using different symbols for readibility.

We want to show that:

$P_1, P_2 \vDash P_1 \land P_2$

using Resolution.

We have to consider the premises and the negation of the conclusion, i.e. the three clauses:

$\{ P_1 \}, \{ P_2 \}$ and $\{ \lnot P_1 \lor \lnot P_2 \}$.

Two applications of the resolution rule are sufficient to produce the empty clause.

Resolution is a proof procedure that is complete meaning that:

for every set of premises $Γ$, any formula that semantically follows from $Γ$ is derivable from $Γ$.

In the example above, conclusion $P_1 \land P_2$ follows from premises $P_1$ and $P_2$. Applying the procedure we have derived the empty clause, showing that the set of clauses with the premises and the negation of the original conlusion is unsatisfiable, which amounts to saying that the original conclusion is a consequence of the premises.

| cite | improve this answer | |
  • $\begingroup$ So,the resolution is complete in the sense that it allows to "completely" check whether a formula is a consequence of another formula but is is not "complete" in the sense that it does allow, as an algorithm, to derive any consequence... How should I say it, one cannot derive all consequence of a formula by blindly using the resolution rule repeatedly? $\endgroup$ – Marc Dinh May 7 at 10:43
  • $\begingroup$ Thanks, I understand. I think that the word derivable is confusing for me since you need to "guess" the consequence before you can apply the resolution method. It is why I put the word "check" in my above comment. $\endgroup$ – Marc Dinh May 7 at 10:55
  • $\begingroup$ @MarcDinh - not necessarily "to guess". You can apply the procedure to $P_1,P_2$ and conclusion $P_1 \land R$: the procedure will stop without producing the empty clause and this means that the third formula does not follow from the two premises. $\endgroup$ – Mauro ALLEGRANZA May 7 at 11:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.