×

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].

MSC:

03F20 Complexity of proofs
68Q15 Complexity classes (hierarchies, relations among complexity classes, etc.)
03B35 Mechanization of proofs and logical operations
PDFBibTeX XMLCite