Abstract
We examine existing resolution systems for quantifed Boolean
formulas (QBF) and answer the question which of these calculi can be
lifted to the more powerful Dependency QBFs (DQBF). An interesting
picture emerges: While for QBF we have the strict chain of proof systems
Q-Res < IR-calc < IRM-calc, the situation is quite different in DQBF.
The obvious adaptations of Q-Res and likewise universal resolution are
too weak: they are not complete. The obvious adaptation of IR-calc has
the right strength: it is sound and complete. IRM-calc is too strong: it is
not sound any more, and the same applies to long-distance resolution.
Conceptually, we use the relation of DQBF to effectively propositional
logic (EPR) and explain our new DQBF calculus based on IR-calc as a
subsystem of frst-order resolution.
Original language | English |
---|---|
Title of host publication | Theory and Applications of Satisfiability Testing – SAT 2016 |
Subtitle of host publication | 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings |
Editors | Nadia Creignou, Daniel Le Berre |
Publisher | Springer Nature |
Pages | 490-499 |
Number of pages | 10 |
Volume | 9710 |
ISBN (Electronic) | 978-3-319-40970-2 |
ISBN (Print) | 978-3-319-40969-6 |
DOIs | |
Publication status | Published - 2016 |