Proof complexity of systems of (non-deterministic) decision trees and branching programs
Abstract
This paper studies propositional proof systems in which lines are sequents of decision trees or branching programs - deterministic and nondeterministic. The systems LDT and LNDT are propositional proof systems in which lines represent deterministic or non-deterministic decision trees. Branching programs are modeled as decision dags. Adding extension to LDT and LNDT gives systems eLDT and eLNDT in which lines represent deterministic and non-deterministic branching programs, respectively. Deterministic and non-deterministic branching programs correspond to log-space (L) and nondeterministic log-space (NL). Thus the systems eLDT and eLNDT are propositional proof systems that reason with (nonuniform) L and NL properties. The main results of the paper are simulation and non-simulation results for tree-like and dag-like proofs in the systems LDT, LNDT, eLDT, and eLNDT. These systems are also compared with Frege systems, constantdepth Frege systems and extended Frege systems
Keywords
Cite
@article{arxiv.1910.08503,
title = {Proof complexity of systems of (non-deterministic) decision trees and branching programs},
author = {Sam Buss and Anupam Das and Alexander Knop},
journal= {arXiv preprint arXiv:1910.08503},
year = {2019}
}
Comments
36 pages, 1 figure, full version of CSL 2020 paper