Proof complexity of systems of (non-deterministic) decision trees and branching programs

Sam Buss, Anupam Das, Alexander Knop

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

2 Citations (Scopus)
69 Downloads (Pure)


This paper studies propositional proof systems in which lines are sequents of decision trees or branching programs, deterministic or non-deterministic. Decision trees (DTs) are represented by a natural term syntax, inducing the system LDT, and non-determinism is modelled by including disjunction, ν, as primitive (system LNDT). Branching programs generalise DTs to dag-like structures and are duly handled by extension variables in our setting, as is common in proof complexity (systems eLDT and eLNDT).

Deterministic and non-deterministic branching programs are natural nonuniform analogues of log-space (L) and nondeterministic log-space (NL), respectively. Thus eLDT and eLNDT serve as natural systems of reasoning corresponding to L and NL, respectively.

The main results of the paper are simulation and non-simulation results for tree-like and dag-like proofs in LDT,LNDT, eLDT and eLNDT. We also compare them with Frege systems, constant-depth Frege systems and extended Frege systems.
Original languageEnglish
Title of host publication28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
EditorsMaribel Fernandez, Anca Muscholl
PublisherSchloss Dagstuhl
Number of pages17
ISBN (Electronic)9783959771320
Publication statusPublished - 6 Jan 2020
Event28th EACSL Annual Conference on Computer Science Logic (CSL 2020) - Barcelona, Spain
Duration: 13 Jan 202016 Jan 2020

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dastuhl
ISSN (Electronic)1868-8969


Conference28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Bibliographical note

Funding Information:
Funding Sam Buss: This work supported in part by Simons Foundation grant 578919. Anupam Das: This work was supported by a Marie Skłodowska-Curie fellowship, Monotonicity in Logic and Complexity, ERC project 753431.

Publisher Copyright:
© Sam Buss, Anupam Das, and Alexander Knop.


  • proof complexity
  • decision trees
  • branching programs
  • logspace
  • sequent calculus
  • non-determinism
  • low-depth complexity

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Proof complexity of systems of (non-deterministic) decision trees and branching programs'. Together they form a unique fingerprint.

Cite this