loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
21st Annual IEEE Symposium on Logic in Computer Science (LICS'06)
Conditional Lower Bound for a System of Constant-Depth Proofs with Modular Connectives
Seattle, Washington
August 12-August 15
ISBN: 0-7695-2631-4
Alexis Maciel, Clarkson University, USA
Toniann Pitassi, University of Toronto, Canada
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.
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
Usage of this product signifies your acceptance of the Terms of Use.