Certification for Quantified Boolean Formulas (QBF) and Dependency Quantified Boolean Formulas is an ongoing challenge (DQBF). 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 obvious 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 make a theoretical observation, that potentially makes this next step in certification easier. We observe that adding a new dependency scheme rule to the checking format DQRAT is p-equivalent to the inclusion of the independent extension variable. Our new dependency scheme rule, the pure-universal dependency scheme (D?pure) shares many similarities to tautology-free dependency schemes, but is special enough not to be covered in the previous literature.

In addition to soundness we show D?pure has two other properties that have been found for previous dependency schemes, and each of these observations has potential in solving/checking. We demonstrate a strategy extraction theorem for LD-Q-resolution equipped with D?pure, meaning it can be incorporated soundly into the dependency learning solver Qute. And we also demonstrate how D?pure can be incorporated in the same way Extended Universal Reduction has used previous dependency schemes.