Open Collections

Proof Complexity of Systems of (Non-Deterministic) Decision Trees and Branching Programs

Banff International Research Station for Mathematical Innovation and Discovery

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. This talk is based on work published in the proceedings of CSL 2020.

Mathematics; Computer science; Mathematical logic and foundations; Theoretical computer science

video/mp4

Author affiliation: UC San Diego

2020-09-18

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/76075

Unreviewed

http://creativecommons.org/licenses/by-nc-nd/4.0/