Refutation (Propositional Resolution)

propositional-logic resolution proof-theory

Definition

Refutation (Propositional Resolution)

A refutation of a set of clauses $KB$ is a derivation from $KB$ that derives the empty clause $\square$.

Since $\square$ is unsatisfiable, a refutation proves that $KB$ is unsatisfiable. In proof by refutation, this is used to prove an entailment by deriving $\square$ from $KB\cup \{\neg A\}$.

Duality

Refutation principle

Proof by refutation is justified by the entailment–unsatisfiability duality:

$$KB\models A\text{if and only if}KB\cup \{\neg A\}\text{ is unsatisfiable}.$$

Thus, to prove $KB\models A$, it is enough to derive a contradiction from $KB\cup \{\neg A\}$.

Method

Proof by refutation

To prove $KB\models A$ by refutation:

1. Negate the goal and form $KB\cup \{\neg A\}$.
2. Transform $KB\cup \{\neg A\}$ into CNF, or into an equisatisfiable clausal normal form.
3. Derive new clauses using the propositional resolution calculus, usually by resolution and factoring.
4. If $\square$ is derived, conclude that $KB\cup \{\neg A\}$ is unsatisfiable.
5. Therefore $KB\models A$.

If no contradiction is derived, this alone does not prove entailment. In a complete refutation procedure, failure to derive $\square$ may instead indicate satisfiability of the clause set.

Examples

Example

Given

$$\neg A\vee B,A\vee B,\neg C\vee \neg B,C$$

the derivation is then:

1. $\neg A\vee B$ (given)
2. $A\vee B$ (given)
3. $\neg C\vee \neg B$ (given)
4. $C$ (given)
5. $B\vee B$ (resolution 2. into 1.)
6. $B$ (factoring 5.)
7. $\neg C$ (resolution 6. into 3.)
8. $\square$ (resolution 4. into 7.)

Example

Either Carlo or Maria killed Mr. X. However, if Carlo would have done it, the alarm would have gone off, and the alarm did not go off. Therefore, Maria killed Mr. X.

$$(C\vee M),(C\to A),\neg A⊢M$$