@ARTICLE{BeyersdorffBlinkhornChewSchmidtSuda19,
AUTHOR = {Beyersdorff, O. and Blinkhorn, J. and Chew, L. and Schmidt, R. A. and Suda, M.},
YEAR = {2019},
TITLE = {Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in {DQBF}},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {63},
NUMBER = {3},
PAGES = {597--623},
DOI = {10.1007/s10817-018-9482-4},
URL = {https://doi.org/10.1007/s10817-018-9482-4},
ABSTRACT = {
Dependency quantified Boolean formulas (DQBF) and QBF dependency
schemes have been treated separately in the literature, even though
both treatments extend QBF by replacing the linear order of the
quantifier prefix with a partial order. We propose to merge the two,
by reinterpreting a dependency scheme as a mapping from QBF into DQBF.
Our approach offers a fresh insight on the nature of soundness in
proof systems for QBF with dependency schemes, in which a natural
property called ‘full exhibition’ is central. We apply our approach to
QBF proof systems from two distinct paradigms, termed ‘universal
reduction’ and ‘universal expansion’. We show that full exhibition is
sufficient (but not necessary) for soundness in universal reduction
systems for QBF with dependency schemes, whereas for expansion systems
the same property characterises soundness exactly. We prove our
results by investigating DQBF proof systems, and then employing our
reinterpretation of dependency schemes. Finally, we show that the
reflexive resolution path dependency scheme is fully exhibited,
thereby proving a conjecture of Slivovsky.
},
}