Understanding Gentzen and Frege Systems for QBF
Olaf Beyersdorff, Ján Pich · 2016
Recently Beyersdorff, Bonacina, and Chew [10] introduced a natural class of Frege systems for quantified Boolean formulas (QBF) and showed strong lower bounds for restricted versions of these systems. Here we provide a comprehensive analysis of the new extended Frege system from [10], denoted EF + ∀red, which is a natural extension of classical extended Frege EF.