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

Sam Buss, Anupam Das, Alexander Knop

Research output: Working paper/PreprintPreprint

3 Downloads (Pure)

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
Original languageEnglish
Publication statusPublished - 18 Oct 2019

Bibliographical note

36 pages, 1 figure, full version of CSL 2020 paper

Keywords

  • cs.CC
  • cs.LO
  • math.LO

Fingerprint

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