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