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

摘要

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 precedures considered are resolution, regular resolution, Davis Putnam procedure, resolution with extension, bounded (and iterated bounded) resolution, enumeration procedures, and semantic trees. The results include exponential lower bounds for the run-time of most of the procedures, relations between the various procedures, and implications to the complexity of integer programming routines.