Lifting lower bounds for tree-like proofs |
| |
Authors: | Alexis Maciel Phuong Nguyen Toniann Pitassi |
| |
Affiliation: | 1. Department of Computer Science, Clarkson University, Postdam, NY, USA 2. School of Computer Science, McGill University, Montreal, QC, Canada 3. Department of Computer Science, University of Toronto, Toronto, ON, Canada
|
| |
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 tree-like 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 exponential lower bounds for such proofs. We prove these lower bounds directly from the computational hardness assumption. We start with a lower bound for cut-free proofs and “lift” it so it applies to proofs with constant-depth cuts. 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 modular connectives are not used. We establish a conditional exponential separation between the power of constant-depth proofs that use different modular connectives. We show that these tree-like proofs with constant-depth cuts cannot polynomially simulate similar dag-like proofs, even when the dag-like proofs are cut-free. We present a new proof of the non-finite axiomatizability of the theory of bounded arithmetic I Δ0(R). Finally, under a plausible hardness assumption concerning the polynomial-time hierarchy, we show that the hierarchy ({G_i^*}) of quantified propositional proof systems does not collapse. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|