SKEDSOFT

Therefore, the clause set is unsatisfiable. Hence the original (unnegated) formula is valid. Figures 2.6 and 2.7 show two versions of a deduction tree corresponding to this deduction.

This resolution theorem forms the basis of most software tools for determining satisfiability of propositional logic formulas. However, the complexity of these tools remains exponential in the original size of the clause set. Chapter 4 presents more efficient representations of boolean formulas using binary decision diagrams (BDDs) that allow faster manipulation of formulas in a number of practical cases.