Sam Buss, Anupam Das, and Alexander Knop
    Proof Complexity of (Non-deterministic) Decison Trees and Branching Programs
    in Proceeedings 28th Conference on Computer Science Logic (CSL), LIPIcs 137 (2020), 12:1-12:17.

    Download draft of full version.

    Download CSL version (extended abstract).

Related talk: Download slides
    Propositional Branching Program Proofs and Logics for L and NL,
    Prague Logic Seminar, November 2020.

Abstract: 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.

Back to Sam Buss's publications page.