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

Sam Buss, Anupam Das, Alexander Knop

Research output: Chapter in Book/Report/Conference proceedingConference contribution

63 Downloads (Pure)

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.
Original languageEnglish
Title of host publication28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
EditorsMaribel Fernández, Anca Muscholl
PublisherSchloss Dagstuhl
Pages12:1-12:17
Number of pages17
ISBN (Print)9783959771320
DOIs
Publication statusPublished - 31 Dec 2019
Event28th EACSL Annual Conference on Computer Science Logic (CSL 2020) - Barcelona, Spain
Duration: 13 Jan 202016 Jan 2020

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dastuhl
Volume152
ISSN (Electronic)1868-8969

Conference

Conference28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
Country/TerritorySpain
CityBarcelona
Period13/01/2016/01/20

Keywords

  • proof complexity
  • decision trees
  • branching programs
  • logspace
  • sequent calculus
  • non-determinism
  • low-depth complexity

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