Prover-Adversary games for systems over (non-deterministic) branching programs
This work provides a game-theoretic characterization of proof systems for branching programs, which is of interest to researchers in proof complexity and computational complexity.
The paper introduces Prover-Adversary games for proof systems over deterministic and non-deterministic branching programs, proving polynomial equivalences and a proof complexity version of the Immerman-Szelepcsenyi theorem.
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.