This problem investigates resolution, a method for proving the unsatisfiability of cnf-formulas. Let be a formula in cnf, where the are its clauses. Let . In a resolution step, we take two clauses and in C, which both have some variable occurring positively in one of the clauses and negatively in the other. Thus, and , where the and are literals. We form the new clause and remove repeated literals. Add this new clause to C. Repeat the resolution steps until no additional clauses can be obtained. If the empty clause ( ) is in C, then declare unsatisfiable. Say that resolution is sound if it never declares satisfiable formulas to be unsatisfiable. Say that resolution is complete if all unsatisfiable formulas are declared to be unsatisfiable.
a. Show that resolution is sound and complete.
b. Use part (a) to show that .