The Complexity of Resolution Procedures for Theorem Proving in the Propositional Calculus

Abstract

A comparative study on the complexity of various procedures for proving that a set of clauses is contradictory is described. All the procedures either use the resolution rule in some form or are closely related to procedures which do. Among the procedures considered are 1. resolution 2. regular resolution 3. Davis Putnam procedure 4. resolution with extension 5. bounded (and iterated bounded) resolution 6. enumeration procedures 7. semantic trees. The results include: a. exponential lower bounds for the run-time of most of the procedures, b. realtions between the various procedures, c. implications to the comlexity of integer programming routines.