Accession Number:

ADA014220

Title:

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

Descriptive Note:

Doctoral thesis,

Corporate Author:

CORNELL UNIV ITHACA N Y DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1975-05-01

Pagination or Media Count:

119.0

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 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.

Subject Categories:

  • Theoretical Mathematics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE