homework 2 on knowledge

We give the detailed answer to Exercise 7.17 in the book of AIMA.

7.17 A propositional 2-CNF expression is a conjunction of clauses, each containing exactly 2 literals, e.g.,
$$(A lor B) land (lnot A lor C) land (lnot B lor D) land (lnot C lor G) land (lnot D lor G)$$

a. Prove using resolution that the above sentence entails G.
b. Two clauses are semantically distinct if they are not logically equivalent. How many semantically distinct 2-CNF clauses can be constructed from n proposition symbols?
c. Using your answer to (b), prove that propositional resolution always terminates in time polynomial in n given a 2-CNF sentence containing no more than n distinct symbols.
d. Explain why your argument in (c) does not apply to 3-CNF.

详细的证明请见 pdf.
(Thanks to Lv Feng.)