Some subsystems of constant-depth Frege with parity

Michal Garlik

We consider three families of subsystems of AC^0[2]-Frege proof systems, i.e. propositional proof systems using constant-depth 
formulas with an additional parity connective. In order of increasing strength, the subsystems are: AC^0-Frege with parity axioms 
in De Morgan language (that is, with no parity connectives) and the treelike and daglike versions of systems introduced by 
Krajícek which we call PK^{c}_{d}(\oplus). Exponential lower bounds on proof size of these subsystems are known; we discuss 
some simulations and separations among them. 

Joint work with Leszek Kolodziejczyk.