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.

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

We investigate small-depth threshold circuits for iterated multiplication and related problems. One result is that we can solve this problem with an ACo-connection of TC 3 o -languages, i.e. an ACo-connection of languages recognizable by depth-3 threshold circuits. This can be compared to the best known construction, which uses four levels of threshold gates (but no ACo-circuitry). Similarly, we design small-depth circuits for powering, division and logarithm. Iterated multiplication is then considered in the context of finite fields. Finally, we look at circuits of quasipolynomial size and we establish various normal forms.

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.

The exact complexity of the weak pigeonhole principle is an old and fundamental problem in proof complexity. Using a diagonalization argument, J. B. Paris et al. (J. Symbolic Logic53 (1988), 1235–1244) showed how to prove the weak pigeonhole principle with bounded-depth, quasipolynomial-size proofs. Their argument was further refined by J. Krajı́cek (J. Symbolic Logic59 (1994), 73–86). In this paper, we present a new proof: we show that the weak pigeonhole principle has quasipolynomial-size LK 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.

The notion of a p-variety arises in the algebraic approach to Boolean circuit complexity. It has great significance, since many known and conjectured lower bounds on circuits are equivalent to the assertion that certain classes of semigroups form p-varieties. In this paper, we prove that semigroups of dot-depth one form a p-variety. This example has the following implication: if a Boolean combination of Σ1 formulas, using arbitrary numerical predicates, defines a regular language, one can then find an equivalent Σ1 formula all of whose numerical predicates are regular.

We show that functions with convergent real power series can be well approximated by two classes of polynomial-size small-weight threshold circuits: depth-three circuits with threshold gates on all levels and depth-four circuits with threshold gates on the first two levels and AND–OR gates on the last two. This is done without restricting the input to a fixed closed subinterval of the interval of convergence of the series. We also point out that rational functions and the logarithm of x in base b can be well approximated by the same classes of circuits when both x and b are given as input.

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.

Constant-depth polynomial-size threshold circuits are usually classified according to their total depth. For example, the best known threshold circuits for iterated multiplication and division have depths four and three, respectively. In this paper, the complexity of threshold circuits is investigated from a different point of view: explicit AND, OR gates are allowed in the circuits, and a threshold circuit is said to have majority-depthdif no path traverses more thandthreshold gates. It is then shown that iterated multiplication can be computed by polynomial-size threshold circuits of total depth five but of majority-depth three. Circuits of depth four and majority-depth two are obtained for division and powering. These results rely on a careful implementation of iterated addition and Chinese remaindering. In addition, a simple symbolic calculus for composing circuit classes is developed: this notation allows for a concise and elegant presentation of the results.

We show that for every prime power pk , quasipolynomiaf size 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.

We investigate the complexity of depth-3 threshold circuits with majority gates at the output, possibly negated AND gates at level two, and MODm 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