Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

Proof Complexity Modulo the Polynomial Hierarchy

Proof Complexity Modulo the Polynomial Hierarchy We present and study a framework in which one can present alternation-based lower bounds on proof length in proof systems for quantified Boolean formulas. A key notion in this framework is that of proof system ensemble, which is (essentially) a sequence of proof systems where, for each, proof checking can be performed in the polynomial hierarchy. We introduce a proof system ensemble called relaxing QU-res that is based on the established proof system QU-resolution. Our main results include an exponential separation of the treelike and general versions of relaxing QU-res and an exponential lower bound for relaxing QU-res; these are analogs of classical results in propositional proof complexity. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png ACM Transactions on Computation Theory (TOCT) Association for Computing Machinery

Proof Complexity Modulo the Polynomial Hierarchy

ACM Transactions on Computation Theory (TOCT) , Volume 9 (3): 20 – Sep 18, 2017

Loading next page...
 
/lp/association-for-computing-machinery/proof-complexity-modulo-the-polynomial-hierarchy-fPdUHTwnL5
Publisher
Association for Computing Machinery
Copyright
Copyright © 2017 ACM
ISSN
1942-3454
eISSN
1942-3462
DOI
10.1145/3087534
Publisher site
See Article on Publisher Site

Abstract

We present and study a framework in which one can present alternation-based lower bounds on proof length in proof systems for quantified Boolean formulas. A key notion in this framework is that of proof system ensemble, which is (essentially) a sequence of proof systems where, for each, proof checking can be performed in the polynomial hierarchy. We introduce a proof system ensemble called relaxing QU-res that is based on the established proof system QU-resolution. Our main results include an exponential separation of the treelike and general versions of relaxing QU-res and an exponential lower bound for relaxing QU-res; these are analogs of classical results in propositional proof complexity.

Journal

ACM Transactions on Computation Theory (TOCT)Association for Computing Machinery

Published: Sep 18, 2017

Keywords: Proof complexity

References