We introduce Pudlak-Buss style Prover-Adversary games to characterise proof systems reasoning over deterministic branching programs (BPs) and non-deterministic branching programs (NBPs). Our starting points are the proof systems eLDT and eLNDT, for BPs and NBPs respectively, previously introduced by Buss, Das and Knop. We prove polynomial equivalences between these proof systems and the corresponding games we introduce. This crucially requires access to a form of negation of branching programs which, for NBPs, requires us to formalise a non-uniform version of the Immerman-Szelepcsenyi theorem that coNL = NL. Thanks to the techniques developed, we further obtain a proof complexity theoretic version of Immerman-Szelepcsenyi, showing that eLNDT is polynomially equivalent to systems over boundedly alternating branching programs.

翻译：我们引入了Pudlak-Buss风格的证人与对手博弈，用以刻画针对确定性分支程序（BPs）和非确定性分支程序（NBPs）的推理证明系统。我们的起点是由Buss、Das和Knop先前引入的分别针对BPs和NBPs的证明系统eLDT和eLNDT。我们证明了这些证明系统与我们引入的相应博弈之间存在多项式等价性。这关键需要访问一种分支程序的否定形式，对于NBPs而言，这要求我们形式化一个非均匀版本的Immerman-Szelepcsenyi定理（即coNL = NL）。借助所发展的技术，我们进一步获得了Immerman-Szelepcsenyi定理的一个证明复杂性理论版本，表明eLNDT与基于有界交替分支程序的系统是多项式等价的。