Exercises
131
Example 13. Let S = {p V q, p V -- q, -p v q, -- p V -q}. Give a resolution refutation
for S (plus comments, as noted in Example 12 above).
Solution.
Line Proof Step
Justification
ro
p V q
Element of S
rl
-pvq
Element of S
r2
q
Resolvant of ro and rT on p
r3
p v -q
Element of S
r4
-- p V -q
Element of S
r5
-q
Resolvant of r3 and r4 on p
r6
F
Resolvant of r2 and r5 on q
U
A proof method is sound if everything that is provable is true or satisfiable. Here,
that means that for any set S of clauses, if there is a resolution refutation of S, then S is
unsatisfiable.
A proof method is complete if everything that is true is provable. If there is a resolution
refutation of a set of clauses S, then S is not complete, since some things that are not true
are provable-that is, any set of clauses for which there is a resolution refutation.
rn Exercises
1. Write DNFs and CNFs corresponding to each of the following truth tables:
(a) p
q
r
Truth Value
(b) p
q
r
Truth Value
T
T T
T
T
T T
F
T
T F
T
T
T F
T
T
F
T
T
T
F
T
F
T
F
F
F
T
F
F
T
F
T T
F
F
T
T
F
F
T F
F
F
T
F
F
F
F
T
T
F
F
T
T
F
F
F
F
F
F
F
T
(c) p
q
r
Truth Value
(d) p
q
r
s
Truth Value
T
T T
T
T
T T
T
F
T
T F
T
T
T F
T
F
T
F
T
F
T
T
F
F
T
T F
F
T
T F
T
F
T
F
T
T
F
F
T
T
T
F
F
T
F
F
F
T
T F
T
F
F
T
T
F
T
F
T
T
F
F
F
F
F
F
F
F
T