Refutation

A refutation is a resolution that concludes to a contradiction. That is, a set of premises can be refuted if it can be logically deduced that they are unsatisfiable.

Take the premises: $P\wedge Q$, $\neg P$. That is, we know that $P\wedge Q$ is true, and also $\neg P$ is true.

We can use resolution to show that these premises lead to a contradiction, either by:

• A resolution tree (which uses resolution rules internally):

• Propositional Logic Equivalences:

$$\begin{array}{rl}& (P\wedge Q)\wedge (\neg P)\\ \equiv & (\neg P)\wedge (P\wedge Q)\\ \equiv & (\neg P\wedge P)\wedge Q\\ \equiv & \perp \wedge Q\\ \equiv & \perp \end{array}\text{\hspace{1em}(Commutativity of ∧)(Associativity of ∧)(Contradiction)(Dominance)}$$

If we are able to conclude a contradiction i.e. our final conclusion is equivalent to $\perp$, then we have refuted our premises, or we have obtained a refutation.

Definition §

Resolution Refutation

Under any logic, we say a well-formed formula $P$ has a resolution refutation (or just refutation) if there exists a resolution proof of $\perp$ from $P$. This is written as:

$$P{⊢}_R\perp$$

The actual resolution proof would be of the form:

$$P⊢C_1,C_2,\dots \perp$$

See Resolution Proof for more details

Resolution via Refutation §

One reason this method is so powerful is because of the unsatisfiability theorem:

This means, if we want to prove that some premises $P_1,P_2,\dots P_n$ conclude to some conclusion $C$, we can alternatively just prove that $P_1,\dots P_n,\neg C{⊢}_R\perp$. That is:

$$P_1\dots P_n⊢C⟺P_1\dots P_n,\neg C⊢\perp$$

For example, take the two disjunctive clauses:

$$\{P\}\{Q\}$$

there is no way of ‘directly’ obtaining a resolution proof of $\{P,Q\}$ i.e. we cannot derive $P,Q{⊢}_{R}P\vee Q$.

However we can achieve a ‘roundabout’ way of resolution via refutation by showing that $P,Q,\neg (P\vee Q){⊢}_R\perp$:

$$\{P\}\{Q\}\{\neg (P\vee Q)\}$$

which can be converted by propositional logic equivalences to:

$$\{P\}\{Q\}\{\neg P\wedge \neg Q\}$$

which can be resolved into $\perp$:

$$P,Q,(\neg P\wedge \neg Q)⊢\neg Q,\perp$$

And by the unsatisfiability theorem, this proves that:

$$P,Q{⊢}_{R}P\vee Q$$

This gives rise to the theorem that resolution is refutation-complete

Theorems §

T1: Refutation is equivalent to unsatisfiability

Let $P_{\Sigma }$ be a set of formulae. Then:

$$P_{\Sigma }\models \perp ⟺P_{\Sigma }{⊢}_R\perp$$

• $P_{\Sigma }\models \perp$ means $P_{\Sigma }$ is unsatisfiable
• $P_{\Sigma }{⊢}_R\perp$ means $P_{\Sigma }$ has a refutation