一句话：为确定性与非确定性分支程序上的证明系统 eLDT/eLNDT 引入 Pudlák-Buss 型证明者-对手博弈，并证明二者多项式等价。
本文研究 Buss、Das 与 Knop 提出的、分别面向确定性分支程序（BP）和非确定性分支程序（NBP）的证明系统 eLDT 与 eLNDT。作者引入 Pudlák-Buss 风格的证明者-对手博弈来刻画这些系统，并证明对应证明系统与博弈之间的多项式等价。证明的关键在于为分支程序提供一种否定形式；对 NBP 而言，这需要形式化 Immerman-Szelepcsenyi 定理 coNL = NL 的非一致版本。借助所发展的技术，作者还得到 Immerman-Szelepcsenyi 定理的证明复杂度版本，即 eLNDT 与有界交替分支程序上的证明系统多项式等价。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{DasD26,
title = {Prover-Adversary games for systems over (non-deterministic) branching programs},
author = {Anupam Das and Avgerinos Delkos},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 2},
year = {2026},
doi = {10.46298/lmcs-22(2:18)2026}
}