Abstract
Several calculi for quantified Boolean formulas (QBFs) exist, but relations between them are not yet fully understood. This paper defines a novel calculus, which is resolution-based and enables unification of the principal existing resolution-based QBF calculi, namely Q-resolution, long-distance Q-resolution and the expansion-based calculus Exp+Res. All these calculi play an important role in QBF solving. This paper shows simulation results for the new calculus and some of its variants. Further, we demonstrate how to obtain winning strategies for the universal player from proofs in the calculus. We believe that this new proof system provides an underpinning necessary for formal analysis of modern QBF solvers. © 2014 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Beyersdorff, O., Chew, L., & Janota, M. (2014). On unification of QBF resolution-based calculi. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8635 LNCS, pp. 81–93). Springer Verlag. https://doi.org/10.1007/978-3-662-44465-8_8
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
