A propositional 2CNF expression is a conjunction of clauses, each containing exactly 2 literals, e.g.,

Prove using resolution that the above sentence entails $G$.

Two clauses are semantically distinct if they are not logically equivalent. How many semantically distinct 2CNF clauses can be constructed from $n$ proposition symbols?

Using your answer to (b), prove that propositional resolution always terminates in time polynomial in $n$ given a 2CNF sentence containing no more than $n$ distinct symbols.

Explain why your argument in (c) does not apply to 3CNF.
Answer
Improve This Solution
View Answer