JavaScript is disabled for your browser. Some features of this site may not work without it.
The Complexity of Resolution Procedures for Theorem Proving in the Propositional Calculus

Author
Galil, Zvi
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.
Date Issued
1975-05Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR75-239
Type
technical report