We provide a tight characterisation of proof size in resolution for quantified Boolean formulas (QBF) by circuit complexity. Such a characterisation was previously obtained for a hierarchy of QBF Frege systems (Beyersdorff & Pich, LICS 2016), but leaving open the most important case of QBF resolution. Different from the Frege ... more >>>

The refutation system {Res}_R({PC}_d) is a natural extension of resolution refutation system such that it operates with disjunctions of degree d polynomials over ring R with boolean variables. For d=1, this system is called {Res}_R({lin}). Based on properties of R, {Res}_R({lin}) systems can be too strong to prove lower ... more >>>