Lifting QBF Resolution Calculi to DQBF
Olaf Beyersdorff, Leroy Chew, Renate Schmidt, Martin Suda

TL;DR
This paper investigates how existing QBF resolution calculi can be extended to the more expressive DQBF framework, revealing that IR-calc is both sound and complete for DQBF, unlike other calculi.
Contribution
It introduces a new DQBF calculus based on IR-calc, establishing its soundness and completeness, and analyzes the limitations of other resolution systems in the DQBF setting.
Findings
IR-calc is sound and complete for DQBF
Q-Resolution and universal Resolution are incomplete for DQBF
IRM-calc is unsound in the DQBF context
Abstract
We examine the existing Resolution systems for quantified 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-Resolution < IR-calc < IRM-calc, the situation is quite different in DQBF. Q-Resolution and likewise universal Resolution are too weak: they are not complete. 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 EPR and explain our new DQBF calculus based on IR-calc as a subsystem of FO-Resolution.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Advanced Algebra and Logic
