文章基本信息

标题：Proof Complexity of Systems of (Non-Deterministic) Decision Trees and Branching Programs
本地全文：下载
作者：Sam Buss ; Anupam Das ; Alexander Knop 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：152
页码：1-17
DOI：10.4230/LIPIcs.CSL.2020.12
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：proof complexity; decision trees; branching programs; logspace; sequent calculus; non-determinism; low-depth complexity