We study the parametrisation of QBF resolution calculi by dependency schemes. One of the main problems in this area is to understand for which dependency schemes the resulting calculi are sound. Towards this end we propose a semantic framework for variable independence based on `exhibition' by QBF models, and use it to express a property of dependency schemes called `full exhibition' that is known to be sufficient for soundness in Q-resolution. Introducing a generalised form of the long-distance resolution rule, we propose a complete parametrisation of classical long-distance Q-resolution, and show that full exhibition remains sufficient for soundness. We demonstrate that our approach applies to the current research frontiers by proving that the reflexive resolution path dependency scheme is fully exhibited.

We include a proof that the reflexive resolution path dependency scheme is fully exhibited; the previous version contained the weaker result that the standard dependency scheme is fully exhibited.

We study the parametrization of QBF resolution calculi by dependency schemes. One of the main problems in this area is to understand for which dependency schemes the resulting calculi are sound. Towards this end we propose a semantic framework for variable independence based on `exhibition' by QBF models, and use it to define a property of dependency schemes called `full exhibition'. We prove that all CDCL-based resolution calculi, including Q-resolution, universal and long-distance Q-resolution, are sound when parametrized by a fully exhibited dependency scheme. To illustrate proof of concept, we show that the standard dependency scheme is fully exhibited.