2026-07-22T04:53:58Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11655 2024-03-06T10:48:42Z ddc:004 open_access

Proof Complexity of Systems of (Non-Deterministic) Decision Trees and Branching Programs Buss, Sam Das, Anupam Knop, Alexander proof complexity decision trees branching programs logspace sequent calculus non-determinism low-depth complexity 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sam Buss and Anupam Das and Alexander Knop 2020 Is Part Of LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2020.12 urn:nbn:de:0030-drops-116553 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.12 eng https://creativecommons.org/licenses/by/3.0/legalcode