Frege Systems for Quantified Boolean Logic
OLAF BEYERSDORFF, University of Jena
ILARIO BONACINA, UPC Barcelona                                                 9
LEROY CHEW, University of Leeds
JAN PICH, University of Oxford
We define and investigate Frege systems for quantified Boolean formulas (QBF). For these new proof systems,
we develop a lower bound technique that directly lifts circuit lower bounds for a circuit class C to the QBF
Frege system operating with lines from C . Such a direct tr ...