On ACC 0 [ p k ] Frege proofs
Alexis Maciel, Toniann Pitassi · 1997
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.