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.

We investigate the proof complexity of systems based on positive branching programs, i.e. non-deterministic branching programs (NBPs) where, for any 0-transition between two nodes, there is also a 1-transition. Positive NBPs compute monotone Boolean functions, just like negation-free circuits or formulas, but constitute a positive version of (non-uniform) NL, rather than P or NC1, respectively. The proof complexity of NBPs was investigated in previous work by Buss, Das and Knop, using extension variables to represent the dag-structure, over a language of (non-deterministic) decision trees, yielding the system eLNDT. Our system eLNDT+ is obtained by restricting their systems to a positive syntax, similarly to how the 'monotone sequent calculus' MLK is obtained from the usual sequent calculus LK by restricting to negation-free formulas. Our main result is that eLNDT+ polynomially simulates eLNDT over positive sequents. Our proof method is inspired by a similar result for MLK by Atserias, Galesi and Pudl\'ak, that was recently improved to a bona fide polynomial simulation via works of Je\v{r}\'abek and Buss, Kabanets, Kolokolova and Kouck\'y. Along the way we formalise several properties of counting functions within eLNDT+ by polynomial-size proofs and, as a case study, give explicit polynomial-size poofs of the propositional pigeonhole principle.