Maciel, Alexis; Pitassi, Toniann Towards lower bounds for bounded-depth Frege proofs with modular connectives. (English) Zbl 0891.03027 Beame, Paul W. (ed.) et al., Proof complexity and feasible arithmetics. Papers from the DIMACS workshop, Rutgers, NJ, USA, April 21–24, 1996. Providence, RI: American Mathematical Society. DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 39, 195-227 (1998). Summary: We show that for every prime power \(p^k\), quasipolynomial-size bounded-depth Frege proofs with \(\text{mod }p^k\) counting connectives can be simulated by quasipolynomial-size proofs of depth 3 consisting of a threshold connective at the output, \(\text{mod }p^k\) connectives on level two, and AND connectives 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 connectives, an outstanding open problem. We also discuss possible interesting consequences for propositional theorem proving.For the entire collection see [Zbl 0881.00033]. Cited in 3 Documents MSC: 03F20 Complexity of proofs 68Q15 Complexity classes (hierarchies, relations among complexity classes, etc.) 03B35 Mechanization of proofs and logical operations Keywords:bounded-depth Frege proofs; counting connectives; quasipolynomial-size proofs; threshold connective; lower bounds; modular connectives; propositional theorem proving PDFBibTeX XMLCite \textit{A. Maciel} and \textit{T. Pitassi}, DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 39, 195--227 (1998; Zbl 0891.03027)