Prover-Adversary games for systems over (non-deterministic) branching programs

TL;DR

A proof complexity theoretic version of Immerman-Szelepcsenyi is obtained, showing that eLNDT is polynomially equivalent to systems over boundedly alternating 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.

Figures (2)

• Figure 1: High-level structure of the polynomial simulations for the non-deterministic setting. The right side displays inference systems and proofs therein, while the left side displays game systems and strategies therein. The bold cyan arrow is the most technical, incorporating our formalisation of Immerman-Szelepcsényi.
• Figure 2: NBP for 2-out-of-4 threshold and representation by extension axioms. Here $0$-edges are dotted, and $1$-edges are solid; the multiple $0$-leaves correspond to the same sink.

Theorems & Definitions (7)

• Remark 2.1: Decision variables
• Proposition 2.2: DBLP:conf/csl/BussDasKnopBussDasKnop19:preprint
• Definition 2.3: Extension axioms
• Example 2.4: 2-out-of-4 threshold
• Remark 2.5: $\mathcal{E}$-induction
• Definition 2.6: Semantics of eNDT formulas
• Proposition 2.7: Complexity of $\mathcal{E}$-induction, e.g. DasDel25:pos-bps-journal