Dependency quantified Boolean formulas (DQBF) describe an NEXPTIME-complete generalisation of QBF, which in turn generalises SAT. QRAT is a recently proposed proof system for quantified Boolean formulas (QBF), which simulates the full suite of QBF preprocessing techniques and thus forms a uniform proof checking format for solver verification.

In this ... more >>>

We advance the theory of QBF proof systems by showing the first simulation of the universal checking format QRAT by a theory-friendly system. We show that the sequent system G fully p-simulates QRAT, including the Extended Universal Reduction (EUR) rule which was recently used to show QRAT does not ... more >>>

We show that the QRAT simulation algorithm of $\forall$Exp+Res from [B. Kiesl and M. Seidl, 2019] cannot be lifted to IR-calc.

more >>>

Merge Resolution (MRes [Beyersdorff et al. J. Autom. Reason.'2021] ) is a refutational proof system for quantified Boolean formulas (QBF). Each line of MRes consists of clauses with only existential literals, together with information of countermodels stored as merge maps. As a result, MRes has strategy extraction by design. The ... more >>>