Dependency quantified Boolean formulas (DQBF) describe an NEXPTIME-complete generalisation of QBF, which in turn generalises SAT. QRAT is a recently proposed proof system for quantified Boolean formulas (QBF), which simulates the full suite of QBF preprocessing techniques and thus forms a uniform proof checking format for solver verification.

In this work, we study QRAT in the more general DQBF context, obtaining a sound and complete refutational DQBF proof system that we call DQRAT. We show that DQRAT can simulate the full suite of dedicated DQBF preprocessing techniques, except those relying on defined variables, which we cover with the introduction of a new form of prefix modification. Our work enables generalisations of further QBF preprocessing techniques (e.g. blocked literal elimination) that were not previously considered for DQBF.