Projects per year

## Abstract

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 NC^{1}, 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 language | English |
---|---|

Title of host publication | Revolutions and Revelations in Computability |

Subtitle of host publication | 18th Conference on Computability in Europe, CiE 2022, Swansea, UK, July 11–15, 2022, Proceedings |

Editors | Ulrich Berger, Johanna N.Y. Franklin, Florin Manea, Arno Pauly |

Publisher | Springer |

Pages | 74-87 |

Number of pages | 14 |

Edition | 1 |

ISBN (Electronic) | 9783031087400 |

ISBN (Print) | 9783031087394 |

DOIs | |

Publication status | Published - 26 Jun 2022 |

Event | 18th Conference on Computability in Europe, CiE 2022 - Swansea, United Kingdom Duration: 11 Jul 2022 → 15 Jul 2022 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

Volume | 13359 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | 18th Conference on Computability in Europe, CiE 2022 |
---|---|

Country/Territory | United Kingdom |

City | Swansea |

Period | 11/07/22 → 15/07/22 |

### 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.

## Keywords

- Branching Programs
- Monotone Complexity
- Proof Complexity

## ASJC Scopus subject areas

- Theoretical Computer Science
- General Computer Science

## Fingerprint

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

- 1 Active