As a natural extension of the SAT problem, different proof systems for quantified Boolean formulas (QBF) have been proposed. Many of these extend a propositional system to handle universal quantifiers.

By formalising the construction of the QBF proof system from a propositional proof system, by the addition of the ... more >>>

Resolution over linear equations (introduced in [RT08]) emerged recently as an important object of study. This refutation system, denoted Res(lin$_R$), operates with disjunction of linear equations over a ring $R$. On the one hand, the system captures a natural ``minimal'' extension of resolution in which efficient counting can be achieved; ... more >>>

We prove exponential lower bounds for $k$-DNF resolution on random $3$-CNF formulas throughout the range $k=O(\sqrt{\log n})$ at every constant clause density above the elementary first-moment bound for unsatisfiability. For random $3$-CNFs this improves Alekhnovich's range $k=O(\sqrt{\log n/\log\log n})$, and matches the $O(\sqrt{\log n})$ range obtained by Sofronova and Sokolov ... more >>>