Proof Complexity of Monotone Branching Programs

Anupam Das*, Avgerinos Delkos

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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, 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ák, that was recently improved to a bona fide polynomial simulation via works of Jeřábek and Buss, Kabanets, Kolokolova and Koucký. 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.

Original languageEnglish
Title of host publicationRevolutions and Revelations in Computability
Subtitle of host publication18th Conference on Computability in Europe, CiE 2022, Swansea, UK, July 11–15, 2022, Proceedings
EditorsUlrich Berger, Johanna N.Y. Franklin, Florin Manea, Arno Pauly
Number of pages14
ISBN (Electronic)9783031087400
ISBN (Print)9783031087394
Publication statusPublished - 26 Jun 2022
Event18th Conference on Computability in Europe, CiE 2022 - Swansea, United Kingdom
Duration: 11 Jul 202215 Jul 2022

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference18th Conference on Computability in Europe, CiE 2022
Country/TerritoryUnited Kingdom

Bibliographical note

Funding Information:
Acknowledgments. This work was supported by a UKRI Future Leaders Fellowship, ‘Structure vs Invariants in Proofs’, project reference MR/S035540/1.

Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.


  • Branching Programs
  • Monotone Complexity
  • Proof Complexity

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Proof Complexity of Monotone Branching Programs'. Together they form a unique fingerprint.

Cite this