Logic and Proof Hilary 2016
Lecture: Resolution
James Worrell
In this lecture we introduce a proof calculus for propositional logic. In general, a proof calculus
consists of rules of inference which can be used to derive a series of conclusions from a series of
hypotheses in a mechanical fashion. We study a particularly simple proof calculus, called resolution,
which has only one rule of inference. This extreme simplicity makes it amenable both to automation
and theoretical analysis. The main results in this lecture are the soundness and completeness of
resolution. Roughly speaking, soundness says that everything we prove is valid, while completeness
says that anything valid can be proved.
1 Set Representation of CNF Formulas
To apply resolution to a formula F it is required that F be in CNF. Thus, if necessary, one must
first convert F to CNF using the equivalences introduced in Lecture 2. It is moreover convenient
to regard each clause in a CNF formula as a set of literals and a formula as a set of clauses. For
example, a CNF formula
F = (p1 ∨ ¬p2 ) ∧ (p3 ∨ ¬p4 ∨ p5 ) ∧ (¬p2 )
is represented in the following form:
F = {{p1 , ¬p2 }, {p3 , ¬p4 , p5 }, {¬p2 }} .
Since the elements of a set do not have order or multiplicity, the set representation of CNF
formulas is a normal form modulo the associativity, commutativity, and idempotence of conjunction
and disjunction. For example, the following CNF formulas F, G, H are all represented by the set
{{p3 }, {p1 , ¬p2 }}:
F = (p3 ∧ (p1 ∨ p1 ∨ ¬p2 ) ∧ p3 )
G = ((¬p2 ∨ p1 ∨ ¬p2 ) ∧ (p3 ∨ p3 ))
H = (p3 ∧ (¬p2 ∨ p1 )) .
In the set representation of CNF formulas the empty clause, denoted 2, is equivalent to false
since it is the unit of the disjunction operation1 . Therefore if a CNF formula contains the empty
clause it is equivalent to false, i.e., it is unsatisfiable. By contrast if a CNF formula is the empty
set of clauses then it is equivalent to true (the unit of the conjunction operation).
2 Resolution
Recall that given a literal L the complementary literal L is defined by
def ¬P if L = P
L =
P if L = ¬P .
1
In similar fashion, the sum of the empty set of natural numbers is 0, the unit of the addition operation, and the
product of the empty set of natural numbers is 1, the unit of the multiplication operation.
1
Definition 1. Let C1 and C2 be clauses. A clause R is called a resolvent of C1 and C2 if there
are complementary literals L ∈ C1 and L ∈ C2 such that
R = (C1 \ {L}) ∪ (C2 \ {L}) .
In the situation of Definition 1 we say that R is derived from C1 and C2 by resolution. We
denote this graphically by
C1 C2
R.
For example, {p1 , p3 , ¬p4 } is a resolvent of {p1 , p2 , ¬p4 } and {¬p2 , p3 }, and the empty clause is
a resolvent of {p1 } and {¬p1 }:
{p1 , p2 , ¬p4 } {¬p2 , p3 } {p1 } {¬p1 }
{p1 , p3 , ¬p4 } 2
A derivation (or proof) of a clause C from a set of clauses F is a sequence C1 , C2 , . . . , Cm of
clauses where Cm = C and for each i = 1, 2, . . . , m either Ci ∈ F or Ci is a resolvent of Cj , Ck for
some j, k < i. A derivation of the empty clause 2 from a formula F is called a refutation of F .
Example 2. A resolution refutation of the CNF formula
{{X, ¬Y }, {Y, Z}, {¬X, ¬Y, Z}, {¬Z}}
is as follows:
1. {X, ¬Y } Assumption 5. {¬X, Z} 2,4 Resolution
2. {Y, Z} Assumption 6. {¬Z} Assumption
3. {X, Z} 1,2 Resolution 7. {Z} 3,5 Resolution
4. {¬X, ¬Y, Z} Assumption 8. 2 6,7 Resolution
The same derivation can also be represented by the following proof tree:
{X, ¬Y } {Y, Z} {Y, Z} {¬X, ¬Y, Z}
{X, Z} {¬X, Z}
{Z} {¬Z}
A resolution refutation of a formula F can be seen as a proof that F is unsatisfiable. This will
be made formal in the next section. Resolution can be used to prove entailments by transforming
them to refutations. For example, the refutation in Example 2 can be used to show that
(X ∨ ¬Y ) ∧ (Y ∨ Z) ∧ (¬X ∨ ¬Y ∨ Z) |= Z .
Given a set of clauses F , we are interested in the set of all clauses that can be derived from F
using resolution. We characterise this set abstractly as follows:
2
Definition 3. Let F be a set of clauses. Then Res(F ) is defined as
Res(F ) = F ∪ {R : R is a resolvent of two clauses in F } .
Furthermore we define
Res 0 (F ) = F
Res n+1 (F ) = Res(Res n (F )) for n ≥ 0 ,
and write [
Res ∗ (F ) = Res n (F ) .
n≥0
Proposition 4. C ∈ Res ∗ (F ) if and only if there is a derivation of C from F .
3 Soundness and Completeness
Lemma 5 (Resolution Lemma). Let F be a CNF formula represented as a set of clauses. Suppose
R is a resolvent of two clauses C1 and C2 of F then F ≡ F ∪ {R}.
Proof. Let A be an assignment. It is obvious that if A |= F ∪ {R} then A |= F . We argue the
converse as follows. Suppose A |= F and write R = (C1 \ {L}) ∪ (C2 \ {L}) for some literal L,
where L ∈ C1 and L ∈ C2 . There are two cases:
Case (i): If A |= L then since A |= C2 it follows that A |= C2 \ {L}, and thus A |= R.
Case (ii): If A |= L then since A |= C1 it follows that A |= C1 \ {L}, and thus A |= R.
Soundness says that we only derive a contradiction from an unsatisfiable set of clauses.
Theorem 6 (Soundness). If there is a derivation of 2 from F then F is unsatisfiable.
Proof. Suppose that C1 , C2 , . . . , Cm = 2 is a proof of 2 from F . By repeated applications of the
Resolution Lemma we have that F is equivalent to F ∪ {C1 , C2 , . . . , Cm }. But the latter set of
clauses includes the empty clause and thus is unsatisfiable.
Completeness is the converse of soundness: it says that if a CNF formula F is unsatisfiable
then we can derive the empty clause from F by resolution. Before giving the proof we specialise
the notion of substitution of propositional formulas, introduced in an earlier lecture.
Given a set of clauses F involving a propositional variable P , let F [false/P ] (read “F with false
for P ”) denote that clause set obtained by replacing P everywhere in F with false, replacing ¬P
with true, and then simplifying by applying the unit laws. That is, F [false/P ] arises by deleting P
from all clauses in F that contain P , and removing from F all clauses that contain ¬P (since they
become true). Likewise we define F [true/P ] by deleting all clauses containing P and removing ¬P
from all clauses containing ¬P .
Example 7. If F = {{p1 , p3 }, {¬p1 , p2 }, {¬p2 , p3 }, {¬p3 }}, then F [false/p3 ] = {{p1 }, {¬p1 , p2 }, {¬p2 }}
and F [true/p3 ] = {{¬p1 , p2 }, 2}.
Theorem 8 (Completeness). If F is unsatisfiable then there is a derivation of 2 from F .
3
Proof. The proof is by induction on the number n of different propositional variables in F .
Base case. The base case is that n = 0, i.e., F does not mention any propositional variables.
Then F either contains no clauses or it contains only the empty clause. In the former case F is
equivalent to true. But F is assumed to be unsatisfiable, so it must be that F = {2} and there is
a one-line resolution refutation of F .
Induction step. Suppose that F is an unsatisfiable set of clauses that mentions variables
p1 , p2 , . . . , pn and let F0 := F [false/pn ] and F1 := F [true/pn ].
Since F is unsatisfiable, F0 is also unsatisfiable. Moreover F0 mentions one fewer variable than
F so by the induction hypothesis there is a resolution proof C0 , C1 , . . . , Cm = 2 that derives the
empty clause from F0 . For each clause Ci in the above proof that comes from F0 , either Ci is
already in F or Ci ∪ {pn } is in F . By replacing the deleted copies of pn from the latter type of
clauses and propagating pn through the proof we obtain a new proof C00 , C10 , . . . , Cm0 from F , where
either Cm 0 = 2 or C 0 = {p } (see Example 9). In the first case there is nothing more left to prove,
m n
so we consider the second case: Cm 0 = {p }. Applying similar reasoning to F we can assume
n 1
that there is a proof of {¬pn } from F . Gluing together these two proofs and applying one more
resolution step to {pn } and {¬pn } gives a proof of 2 from F .
Example 9. We illustrate the transformation on proofs underlying the induction step in the proof
of the Completeness Theorem.
Consider the formula F = {{P, R}, {¬P, Q}, {¬Q, R}}. We transform the following derivation
of 2 from F [false/R]
{P } {¬P, Q}
{Q} {¬Q}
to the following derivation of {R} from F :
{P, R} {¬P, Q}
{Q, R} {¬Q, R}
{R}
