134 CHAPTER 2 Formal Logic
(a) 1p, -p V q, --p V -q V r, -•r(b) {-p, p V q, -q v -r, p V r}
(c) {p V q, -'p v r, -q V r, -p V s, -q V s, -r V -x}
(d) {p V q V r, p v q v-r, p v-q v r, p v-q v-r,-p v q V r, -pv q v -r,
-'p V -'q V r, -'p V -'q V -'r}.
- (a) Show that if r is the resolvant of two clauses Cl, c2 on proposition letter p, then
{Cl, C2} = r(Hint: For each interpretation, break into cases, depending on whether p is T or
F in each interpretation.)
(b) Prove that if there is a resolution refutation of a set S of clauses, then S is unsatis-
fiable. (Hint: Use strong induction on the length of the resolution refutation.)- The length of a clause is the number of literals in the clause. The length of a CNF
formula is the sum of the length of its clauses. The number of excess literals in a CNF
formula is the length of the formula minus the number of clauses in the formula.
(a) Show that if an unsatisfiable set S of clauses contains only clauses of length 0 and
1, it has a resolution refutation. (Hint: Prove the following: If S contains a clause
of length 0, it has [trivially] a resolution refutation. If, for some proposition letter
p, S contains both p and --p, then S has a resolution refutation. Otherwise, S is
satisfiable.)
(b) Show that if a set {(; 1 V )2 V ... V X)k V Xk+Il} U S (k > 1) of clauses is un- satisfiable, so are {I 1 V X 2 V Xk} U S and {)k+l} U S. (Hint: For the first half, prove that if an interpretation I satisfies {[) 1 V ) 2 V ... V )1} U S, it also satisfies {) 1 V X 2 V ... V -k V Xk+l} U S.) (c) Show that for k > 1, the number of excess literals in {)1 V X 2 V ... V )k} U S and
the number of excess literals in {)k+ } U S are both less than the number of excess
literals in {A 1 V )` 2 V .. V 4k V k+0} U S.
(d) A resolution derivation of a clause rk from a set S of clauses is a sequence
ro, rl, r2 ..... rk of clauses where each ri is either an element of S or a resolvant
of two previous rj 's. (Thus, resolution refutation of S is just a resolution deriva-
tion of F from S.) Show that if there is a resolution derivation of A from S and a
resolution refutation of S U {[I, then there is a resolution refutation of S.
(e) Prove that if there is a resolution refutation p of {X 1 V X 2 V ... V Ak} U S, then
either (i) there is a resolution refutation of {0 1 V ;A 2 V ... V Ak V 4k+1} U S or
(ii) there is a resolution derivation of Xk+1 from X 1 V X 2 V ... V Ak V Ak+l U S.
(Hint: Prove this by induction on the length p. You will have to add Ak+l as a
disjunct to some of the clauses in p. It is not true in general that if S • A, then
there is a resolution derivation of A` from S.)
(f) Prove that resolution refutation is complete.rnPredicates and Quantification
In propositional logic, our basic "objects" were entire statements, represented by proposi-
tion letters. In discussing mathematical structures, however, we want to be able go one step