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