arXiv · 2508.16014
Prover-Adversary games for systems over (non-deterministic) branching programs
Abstract
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.
Explore related subjects
Keep this discovery
Anupam Das, Avgerinos Delkos. 2025-08-22. Prover-Adversary games for systems over (non-deterministic) branching programs. https://doi.org/10.46298/lmcs-22(2%3A18)2026
Cite the original work for its findings. Save a collection to share your selection of sources.