130 CHAPTER 2 Formal Logic
p v -q and r v qare given. What conclusion is possible for the conjunction of these two clauses as a hy-
pothesis? In the resolution system, we are interested in the implication((p V -,q) A (r V q)) -- (p V r)It is easy to prove using a truth table that this implication is always T. With this inference
rule, we can then use the clause p V r as another clause in the resolution system. The reso-
lution rule uses only this inference rule with formulas in CNE We often display this rule asp V -- q
r Vq
p vr
Definition 4. Let two clauses cl 4 v p and c2 = Vf v -- p be given where p is a propo-
sition letter and 0k and 't are clauses. The resolvant of cl and C2 on p is the clause 01 V V1.Example 11. Let cl = p v --q v r and c2 = -'p v r v s V t. The resolvant of clauses Cl
and C2 on p is-,qvrvrvsvt=--qvrvsvtIn a resolution proof or resolution refutation, we imagine the conjunction of a set of
clauses being the hypothesis for an implication. The resolution rule can be used to see if
the set of clauses is satisfiable. If the conjunction of the set of clauses is F, then the set of
clauses is unsatisfiable. We formalize the idea of this proof technique in the next definition.Definition 5. Let S be a set of clauses. A resolution refutation of S is a sequence of
clauses ro, rl, .... , rk such that:(a) each ri is either an element of S or a resolvant of rj and rk where 0 < j 7• k < i < k,
and
(b) rk = F.Example 12. Let S be the set of clauses {p, -p v --q, -'p v q v r, -,r}. Give a resolu-
tion refutation of S.Solution. The right-hand column of the following table just explains why each step is
valid. The left-hand column simply numbers the lines so that we can refer to them later.Proof Step Clause Justification
ro p Element of S
rl -- p V -q Element of S
r2 --q Resolvant of ro and rl on p
r0 --,p V q V r Element of S
N q V r Resolvant of ro and r3 on p
r5 r Resolvant of r4 and r2 on q
r6 --r Element of S
r7 F Resolvant of r5 and r6 on r U