On Stronger Calculi for QBFs
Abstract
Quantified Boolean formulas (QBFs) generalize propositional formulas by admitting quantifications over propositional variables. QBFs can be viewed as (restricted) formulas of first-order predicate logic and easy translations of QBFs into first-order formulas exist. We analyze different translations and show that first-order resolution combined with such translations can polynomially simulate well-known deduction concepts for QBFs. Furthermore, we extend QBF calculi by the possibility to instantiate a universal variable by an existential variable of smaller level. Combining such an enhanced calculus with the propositional extension rule results in a calculus with a universal quantifier rule which essentially introduces propositional formulas for universal variables. In this way, one can mimic a very general quantifier rule known from sequent systems.
Keywords
Cite
@article{arxiv.1604.06483,
title = {On Stronger Calculi for QBFs},
author = {Uwe Egly},
journal= {arXiv preprint arXiv:1604.06483},
year = {2016}
}