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.)