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}.
15. (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 unsatisfiable. (Hint: Use strong induction on the length of the resolution refutation.)
16. 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 unsatisfiable, 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 derivation 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 proposition letters. In discussing mathematical structures, however, we want to be able go one step
"lower" to assert statements, such as x = 3 or x > y, where the meanings of x and y are
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}.
15. (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 unsatisfiable. (Hint: Use strong induction on the length of the resolution refutation.)
16. 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 unsatisfiable, 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 derivation 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 proposition letters. In discussing mathematical structures, however, we want to be able go one step
"lower" to assert statements, such as x = 3 or x > y, where the meanings of x and y are