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.

翻译：我们分别调查基于正分支程序的系统证明复杂性, 即非确定性分支程序( NBPs ) 。 在两个节点之间的任何 0 过渡中, 也存在一个 1 过渡 。 积极的 NBPs 计算单调布林函数, 就像无否定性电路或公式一样, 但是构成一个积极的版本 NL, 而不是 P 或 NC1 。 Bus、 Das 和 Knop 在先前的工作中调查了 NBPs 的证明复杂性, 使用扩展变量来代表 dag 结构, 超过一个( 非确定性) 决策树的语言, 产生 eLNDT。 我们的 eLNDT+ 函数, 我们的系统 eLNDTT+ 函数通过将系统限制为积极的同步, 类似于“ Monotont 序列的计算”, 而不是 Palcult 。 我们的主要结果是, eNDT+ IPIalal oral realalalalal oral oral oral 。