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.

翻译：我们研究了基于正分支程序的证明系统复杂性，即非确定性分支程序（NBP），其中任意两个节点间的0-转移都伴随一个1-转移。正NBP计算单调布尔函数，类似于无否定电路或公式，但构成了（非均匀）NL的正版本，而非分别对应P或NC¹。Buss、Das和Knop在先前工作中通过扩展变量表示有向无环图结构，在（非确定性）决策树语言上研究了NBP的证明复杂性，建立了eLNDT系统。我们的eLNDT+系统通过将其系统限制于正语法而获得，类似于从常规序列演算LK通过限制为无否定公式得到"单调序列演算"MLK。我们的主要结果是：在正序列上，eLNDT+多项式模拟eLNDT。证明方法受Atserias、Galesi和Pudlák关于MLK的类似结果启发，该结果近期通过Jeřábek以及Buss、Kabanets、Kolokolova和Koucký的工作改进为真正的多项式模拟。在此过程中，我们通过多项式规模证明在eLNDT+内形式化了计数函数的若干性质，并作为案例研究，给出了命题鸽巢原理的显式多项式规模证明。