Discrete Mathematics for Computer Science

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