Resolution

“If you flee from the things you fear, there’s no resolution.”
—Chuck Palahniuk

Resolution is very simple proof system that is the foundation of many of the most successful attempts to have computers prove theorems automatically. However, Resolution proofs are not organized in the way that humans tend to think, and so they are not particularly easy to read or understand.

The Resolution Rule

Definition

The Resolution Rule is

\frac{{\cal A}\lor {\cal B}\qquad \lnot {\cal B}\lor {\cal C}} {{\cal A}\lor {\cal C}}

or more generally,

\frac{{\cal A}_1\lor \cdots\lor {\cal A}_n\lor {\cal B} \qquad \lnot {\cal B}\lor {\cal C}_1\lor\cdots\lor {\cal C}_m} {{\cal A}_1\lor \cdots\lor {\cal A}_n\lor {\cal C}_1\lor\cdots\lor {\cal C}_m}

Here are some concrete examples of applying the (generalized) Resolution Rule. Of note:

We freely reorder disjunctions and throw away duplicate disjuncts (e.g., producing $Q$ instead of $Q \lor Q$ ).
We write the case of zero formulas or’ed together as $\bot$ .

Example

Here are some sample applications of the Resolution Rule.

\begin{array}{lllll} P \lor Q & \mathrm{and} & \lnot Q\lor R & \mathrm{yield} & P \lor R \\[20pt] P \lor Q & \mathrm{and} & R \lor \lnot Q & \mathrm{yield} & P \lor R \\[20pt] P \lor Q & \mathrm{and} & \lnot P \lor Q & \mathrm{yield} & Q \\[20pt] P \lor Q & \mathrm{and} & \lnot P & \mathrm{yield} & Q \\[20pt] R & \mathrm{and} & \lnot R & \mathrm{yield} & \bot \\[20pt] P \lor \lnot Q \lor R& \mathrm{and} & P \lor Q \lor S & \mathrm{yield} & P \lor R \lor S \\ \end{array}

Resolution Proofs

A Resolution proof is simply a list of assumptions, followed by a sequence of applications of the resolution rule, ending with $\bot$ .

Example

Suppose we want to prove $P\lor Q, \ \lnot P\lor R, \lnot R, \lnot Q \vdash \bot$ . One such proof is:

\begin{array}{lll} 1. & P\lor Q & \mathrm{Assumption}\\ 2. & \lnot P\lor R & \mathrm{Assumption}\\ 3. & \lnot R & \mathrm{Assumption}\\ 4. & \lnot Q & \mathrm{Assumption}\\ 5. & Q\lor R & (1,2)\\ 6. & R & (4,5)\\ 7. & \bot & (3,6)\\ \end{array}

In a Resolution proof it suffices to just mention the lines justifying our proof steps. The rule being used is always the Resolution Rule.

Beyond Clauses

There are two objections that one might have to resolution. The first is, “Why are we always proving $\bot$ ?“.

But this is not a restriction, because if we want to prove

{\cal A}_1,\ldots,{\cal A}_n \vdash {\cal B}

it suffices to use Proof by Contradiction and instead prove

{\cal A}_1,\ldots,{\cal A}_n, \lnot {\cal B} \vdash \bot.

The more serious objection is that the resolution rule only works for disjunctions, whereas WFFs can have conjunctions and implications. But this can be solved as well, because every WFF is equivalent to a collection of clauses, and resolution is designed to work with clauses.

Definition

A literal is an atomic formula or its negation

Example

Here are four literals:

P\qquad \lnot Q \qquad R_7\qquad \lnot S'

Definition

A clause is a disjunction of zero or more literals. (Recall that we write the disjunction of zero literals as $\bot$ .)

Example

Here are four clauses:

P\lor S\qquad \lnot P\lor Q\lor \lnot R\qquad \lnot S\qquad \bot

We can convert arbitrary WFFs to clauses using the following steps:

Get rid of implications, e.g., $P\to Q$ becomes $\lnot P\lor Q$ .
Push negations inward, e.g., $\lnot(P\land Q)$ becomes $\lnot P \lor \lnot Q$ .
Distribute $\lor$ over $\land$ , e.g., $a\lor(b\land c)$ becomes $(a\lor b)\land(a\lor c)$ .
Break conjunctions into clauses, e.g., $(a\lor b)\land(a\lor c)$ becomes $a\lor b,\ a\lor c$ .

Then to prove ${\cal A}_1, \ldots, {\cal A}_n\ \vdash\ {\cal B}$ we:

Switch to Proof by Contradiction: ${\cal A}_1, \ldots, {\cal A}_n, \lnot {\cal B}\ \vdash\ \bot$ .
Convert ${\cal A}_1, \ldots, {\cal A}_n$ and $\lnot {\cal B}$ into clauses.
Take these as the starting assumptions.
Apply the Resolution Rule until we reach $\bot$

Example

Prove $P\to Q,\ P\ \vdash\ Q$ .

Proof by Contradiction: Rephrase as $P\to Q,\ P,\ \lnot Q\ \vdash\ \bot$ .

Clauses: $P\to Q$ converts to $\lnot P\lor Q$ , but $P$ and $\lnot Q$ are already clauses.

Proof:

\begin{array}{lll} 1. & \lnot P\lor Q & \mathrm{Assumption}\\ 2. & P & \mathrm{Assumption}\\ 3. & \lnot Q & \mathrm{Assumption}\\ 4. & \lnot P & (1,3)\\ 6. & \bot & (2,4)\\ \end{array}

(Other proofs are possible.)

Example

Prove $P\to Q,\ Q\to R\ \vdash\ P\to R$ .

Proof by Contradiction: Rephrase as $P\to Q,\ Q\to R,\ \lnot(P\to R)\ \vdash\ \bot$ .

Clauses:

$P\to Q$ converts to $\lnot P\lor Q$ ;
$Q\to R$ converts to $\lnot Q\lor R$ ;
$\lnot(P\to R) \equiv (P\land \lnot R)$ converts to the two clauses $P$ and $\lnot R$ .

Proof:

\begin{array}{lll} 1. & \lnot P\lor Q & \mathrm{Assumption}\\ 2. & \lnot Q\lor R & \mathrm{Assumption}\\ 3. & P & \mathrm{Assumption}\\ 4. & \lnot R & \mathrm{Assumption}\\ 5. & Q & (1,3)\\ 6. & R & (2,5)\\ 7. & \bot & (4,6)\\ \end{array}

(Other proofs are possible.)

Metatheory

Theorem

The Resolution Rule is sound and complete for classical propositional logic (once we have converted everything into equivalent clauses).