|
Published Articles >> Table of Contents >> Abstract
21st Annual IEEE Symposium on Logic in Computer Science (LICS'06)
pp. 189-200
Conditional Lower Bound for a System of Constant-Depth Proofs with Modular Connectives
Alexis Maciel, Clarkson University, USA
Toniann Pitassi, University of Toronto, Canada
Full Article Text:
 
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2006.19
Send link to a friend
| Abstract |
|
It is known that constant-depth Frege proofs of some tautologies
require exponential size. No such lower bound
result is known for more general proof systems. We consider
Sequent Calculus proofs in which formulas can contain
modular connectives and only the cut formulas are restricted
to be of constant depth. Under a plausible hardness
assumption concerning small-depth Boolean circuits, we
prove an exponential lower bound for such proofs. We prove
this lower bound directly from the computational hardness
assumption. By using the same approach, we obtain the
following additional results. We provide a much simpler
proof of a known (unconditional) lower bound in the case
where only conjunctions and disjunctions are allowed. We
establish a conditional exponential separation between the
power of constant-depth proofs that use different modular
connectives. Finally, under a plausible hardness assumption
concerning the polynomial-time hierarchy G \frac{*}{i}, we show
that the hierarchy of quantified propositional proof systems
does not collapse.
|
 Additional Information
|
Citation:
Alexis Maciel, Toniann Pitassi,
"Conditional Lower Bound for a System of Constant-Depth Proofs with Modular Connectives,"
lics,
pp. 189-200,
21st Annual IEEE Symposium on Logic in Computer Science (LICS'06),
2006
|
|
