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, we show that the hierarchy Gi* of quantified propositional proof systems does not collapse

The exact complexity of the weak pigeonhole principle is an old and fundamental problem in proof complexity.Using a diagonalization argument, Paris, Wilkie and Woods [9] showed how to prove the weak pigeonhole principle with bounded-depth, quasipolynomial-size proofs.Their argument was further refined by Krajf~ek [5].In this paper, we present a new proof: we show that the the weak pigeonhole principle has quasipolynomial-size proofs where every formula consists of a single AND/OR. of polylog fan-in.Our proof is conceptually simpler than previous arguments, and is optimal with respect to depth.

Since the publication of M. Furst et al. (1984) seminal paper connecting AC/sup 0/ with the polynomial hierarchy, it has been well known that circuit lower bounds allow you to construct oracles that separate complexity classes. We show that similar circuit lower bounds allow you to construct oracles that collapse complexity classes. For example, based on Hastad's parity lower bound, we construct an oracle such that P=PH/spl sub//spl oplus/P=EXP.

In this paper; we show how to extend the argument due to Bonet, Pitassi and Raz to show that bounded-depth Frege proofs do not have feasible interpolation, assuming that factoring of Blum integers or computing the Diffie-Hellman function is sufficiently hard. It follows as a corollary that bounded-depth Frege is not automatizable; in other words, there is no deterministic polynomial-time algorithm that will output a short proof if one exists. A notable feature of our argument is its simplicity.

We investigate the complexity of depth-3 threshold circuits with majority gates at the output, possibly negated AND gates at level two, and MOD/sub m/ gates at level one. We show that the fan-in of the AND gates can be reduced to O(log n) in the case where m is unbounded, and to a constant in the case where m is constant. We then use these upper bounds to derive exponential lower bounds for this class of circuits. In the unbounded m case, this yields a new proof of a lower bound of Grolmusz; in the constant m case, our result sharpens his lower bound. In addition, we prove an exponential lower bound if OR gates are also permitted on level two and m is a constant prime power.

We show that for every prime power pk , quasipolynomiafsize bounded-depth Frege proofs with mod pk counting comectives can be simulated by quasipolynomiaf-size proofs of depth 3 consisting of a threshold connective at the output, mod pk connective on level two, and AND connective of small fan-in on level one.We argue that this result is a plausible first step towards proving lower bounds for bounded-depth Frege proofs with modular connective, an outstanding open problem.We also discuss possible int cresting consequences for automated theorem proving.