Pool resolution is NP-hard to recognize

Archive for Mathematical Logic 48 (8):793-798 (2009)
  Copy   BIBTEX

Abstract

A pool resolution proof is a dag-like resolution proof which admits a depth-first traversal tree in which no variable is used as a resolution variable twice on any branch. The problem of determining whether a given dag-like resolution proof is a valid pool resolution proof is shown to be NP-complete

Categories

Keywords

Reprint years

DOI

10.1007/s00153-009-0152-4

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,881

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

The Depth of Resolution Proofs.Alasdair Urquhart - 2011 - Studia Logica 99 (1-3):349-364.
Resolution calculus for the first order linear logic.Grigori Mints - 1993 - Journal of Logic, Language and Information 2 (1):59-83.
Minimum propositional proof length is NP-Hard to linearly approximate.Michael Alekhnovich, Sam Buss, Shlomo Moran & Toniann Pitassi - 2001 - Journal of Symbolic Logic 66 (1):171-191.
The Complexity of Resolution Refinements.Joshua Buresh-Oppenheim & Toniann Pitassi - 2007 - Journal of Symbolic Logic 72 (4):1336 - 1352.
Resolution and the origins of structural reasoning: Early proof-theoretic ideas of Hertz and Gentzen.Peter Schroeder-Heister - 2002 - Bulletin of Symbolic Logic 8 (2):246-265.
Resolution for Intuitionistic Logic.Melvin Fitting - unknown
A note on propositional proof complexity of some Ramsey-type statements.Jan Krajíček - 2011 - Archive for Mathematical Logic 50 (1-2):245-255.
Extracting the resolution algorithm from a completeness proof for the propositional calculus.Robert Constable & Wojciech Moczydłowski - 2010 - Annals of Pure and Applied Logic 161 (3):337-348.
The complexity of propositional proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.
Interpolation theorems, lower Bounds for proof systems, and independence results for bounded arithmetic.Jan Krajíček - 1997 - Journal of Symbolic Logic 62 (2):457-486.
Relative efficiency of propositional proof systems: resolution vs. cut-free LK.Noriko H. Arai - 2000 - Annals of Pure and Applied Logic 104 (1-3):3-16.

Analytics

Added to PP
2013-11-23

Downloads
57 (#281,003)

6 months
12 (#213,833)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

Add more references