Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF

Area of Science:

• Automated Reasoning
• Computational Logic
• Theoretical Computer Science

Background:

• Dependency quantified Boolean formulas (DQBF) and QBF dependency schemes are distinct yet related extensions of QBF.
• Both formalisms replace linear quantifier order with partial orders, enabling more expressive reasoning.
• Existing literature treats these concepts separately, hindering a unified understanding of their proof systems.

Purpose of the Study:

• To unify the treatment of DQBF and QBF dependency schemes.
• To reinterpret dependency schemes as mappings from QBF to DQBF.
• To gain new insights into the soundness of proof systems for QBF with dependency schemes.

Main Methods:

• Reinterpreting dependency schemes as mappings into DQBF.
• Investigating DQBF proof systems.
• Applying the reinterpretation to analyze soundness properties ('full exhibition') in universal reduction and universal expansion paradigms.

Main Results:

• Full exhibition is sufficient but not necessary for soundness in universal reduction systems.
• Full exhibition exactly characterizes soundness in universal expansion systems.
• The reflexive resolution path dependency scheme is demonstrated to be fully exhibited.

Conclusions:

• The proposed reinterpretation provides a unified framework for DQBF and QBF dependency schemes.
• The property of 'full exhibition' plays a crucial role in characterizing soundness across different proof system paradigms.
• A long-standing conjecture by Slivovsky regarding the reflexive resolution path dependency scheme is proven.