Lesson 3

One of the basic proof systems studied is called resolution. The unsatisfiability of a given CNF formula \(F\) in this system can be proved as follows. Let the set \(\mathcal{C}\) equal the set of clauses of the formula \(F\). Then, in one step, we can take two clauses \((A \lor l)\) and \((B \lor \overline{l})\) from the set \(\mathcal{C}\) and derive from them the clause \((A \lor B)\). The new clause is added to the set \(\mathcal{C}\) and the process continues. If in this way we succeed in deriving the empty clause from the original set of clauses, then the original formula is unsatisfiable.

It is known that this proof system is sound (if the empty clause is derived, then the formula is unsatisfiable) and complete (from any unsatisfiable formula one can derive the empty clause).