Lifting QBF Resolution Calculi to DQBF

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.