The Complexity of Resolution Procedures for Theorem Proving in the Propositional Calculus.
CORNELL UNIV ITHACA N Y DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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.
- Theoretical Mathematics