Proof complexity of systems of (non-deterministic) decision trees and branching programs
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Documents
- OA-Proof Complexity of Systems of
Final published version, 543 KB, PDF document
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 language | English |
---|---|
Title of host publication | 28th EACSL Annual Conference on Computer Science Logic, CSL 2020 |
Editors | Maribel Fernandez, Anca Muscholl |
Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
Publication date | Jan 2020 |
Article number | 12 |
ISBN (Electronic) | 9783959771320 |
DOIs | |
Publication status | Published - Jan 2020 |
Event | 28th EACSL Annual Conference on Computer Science Logic, CSL 2020 - Barcelona, Spain Duration: 13 Jan 2020 → 16 Jan 2020 |
Conference
Conference | 28th EACSL Annual Conference on Computer Science Logic, CSL 2020 |
---|---|
Land | Spain |
By | Barcelona |
Periode | 13/01/2020 → 16/01/2020 |
Series | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|
Volume | 152 |
ISSN | 1868-8969 |
- Branching programs, Decision trees, Logspace, Low-depth complexity, Non-determinism, Proof complexity, Sequent calculus
Research areas
ID: 250488419