The Complexity of Resolution Refinements

Journal of Symbolic Logic 72 (4):1336 - 1352 (2007)

Resolution is the most widely studied approach to propositional theorem proving. In developing efficient resolution-based algorithms, dozens of variants and refinements of resolution have been studied from both the empirical and analytic sides. The most prominent of these refinements are: DP (ordered). DLL (tree), semantic, negative, linear and regular resolution. In this paper, we characterize and study these six refinements of resolution. We give a nearly complete characterization of the relative complexities of all six refinements. While many of the important separations and simulations were already known, many new ones are presented in this paper: in particular, we give the first separation of semantic resolution from general resolution. As a special case, we obtain the first exponential separation of negative resolution from general resolution. We also attempt to present a unifying framework for studying all of these refinements
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2178/jsl/1203350790
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 48,902
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

The Complexity of Propositional Proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles


Added to PP index

Total views
42 ( #219,892 of 2,309,716 )

Recent downloads (6 months)
1 ( #758,532 of 2,309,716 )

How can I increase my downloads?


My notes

Sign in to use this feature