Certification for Quantified Boolean Formulas (QBF) and Dependency Quantified Boolean Formulas (DQBF) is an ongoing challenge. Recent proof complexity work has shown that the majority of QBF and DQBF techniques can be p-simulated by using the independent extension rule. In propositional logic, extension rules are supported by proof checkers using a more general RAT (Resolution Asymmetric Tautology) rule. The next step in (D)QBF certification would be to update these modern RAT formats to match the strength of this independent extension rule. In this paper we first introduce a new dependency scheme called Dpure. This rule is the missing ingredient that when added to Blinkhorn's proof system DQRAT allows it to be provably p-equivalent to the Independent Extended QU-Res, the most powerful of the known QBF and DQBF proof systems. Up until now, DQRAT has only existed in theory, so we implement a prototype checker DQRAT-check which includes our extra rule. In addition to its inclusion in our proof checker we show Dpure has other properties that have been found for previous dependency schemes, and each of these observations has potential in solving/checking including the sound integration into the dependency learning solver Qute.

翻译：量化布尔公式（QBF）和依赖量化布尔公式（DQBF）的认证是一个持续存在的挑战。最近的证明复杂性研究表明，大多数QBF和DQBF技术可以通过使用独立扩展规则进行p-模拟。在命题逻辑中，扩展规则由证明检查器通过更通用的RAT（分解非对称重言式）规则支持。(D)QBF认证的下一步将是更新这些现代RAT格式，以匹配这种独立扩展规则的强度。在本文中，我们首先引入一种名为Dpure的新依赖方案。该规则是缺失的要素，将其添加到Blinkhorn的证明系统DQRAT中时，可以使其被证明与独立的扩展QU-Res（已知最强大的QBF和DQBF证明系统之一）p-等价。迄今为止，DQRAT仅存在于理论中，因此我们实现了一个原型检查器DQRAT-check，其中包含我们的额外规则。除了将其纳入我们的证明检查器外，我们还展示了Dpure具有先前依赖方案中发现的其他特性，每个这些观察结果在求解/检查中都具有潜力，包括与依赖学习求解器Qute的可靠集成。