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

Sam Buss; Anupam Das; Alexander Knop

doi:10.4230/LIPIcs.CSL.2020.12

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

Sam Buss, Anupam Das, Alexander Knop

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

2 Citations (Scopus)

93 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 language	English
Title of host publication	28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
Editors	Maribel Fernandez, Anca Muscholl
Publisher	Schloss Dagstuhl
Number of pages	17
ISBN (Electronic)	9783959771320
DOIs	https://doi.org/10.4230/LIPIcs.CSL.2020.12
Publication status	Published - 6 Jan 2020
Event	28th EACSL Annual Conference on Computer Science Logic (CSL 2020) - Barcelona, Spain Duration: 13 Jan 2020 → 16 Jan 2020

Publication series

Name	Leibniz International Proceedings in Informatics (LIPIcs)
Publisher	Schloss Dastuhl
Volume	152
ISSN (Electronic)	1868-8969

Conference

Conference	28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
Country/Territory	Spain
City	Barcelona
Period	13/01/20 → 16/01/20

Bibliographical note

Funding Information:
Funding Sam Buss: This work supported in part by Simons Foundation grant 578919. Anupam Das: This work was supported by a Marie Skłodowska-Curie fellowship, Monotonicity in Logic and Complexity, ERC project 753431.

Publisher Copyright:
© Sam Buss, Anupam Das, and Alexander Knop.

Keywords

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

ASJC Scopus subject areas

Software

Access to Document

10.4230/LIPIcs.CSL.2020.12Licence: Creative Commons: Attribution (CC BY)

Buss_et_al_Proof_complexity_of_systems_of_non-deterministic_decision_trees_and_branching_programs_LIPIcs_CSL_2020Final published version, 543 KBLicence: Creative Commons: Attribution (CC BY)

https://drops.dagstuhl.de/opus/volltexte/2020/11655/Licence: Creative Commons: Attribution (CC BY)

Cite this

Buss, S., Das, A., & Knop, A. (2020). Proof complexity of systems of (non-deterministic) decision trees and branching programs. In M. Fernandez, & A. Muscholl (Eds.), 28th EACSL Annual Conference on Computer Science Logic (CSL 2020) Article 12 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 152). Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.CSL.2020.12

@inproceedings{761da2b5262747778dba38c1bf6a197f,

title = "Proof complexity of systems of (non-deterministic) decision trees and branching programs",

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.",

keywords = "proof complexity, decision trees, branching programs, logspace, sequent calculus, non-determinism, low-depth complexity",

author = "Sam Buss and Anupam Das and Alexander Knop",

note = "Funding Information: Funding Sam Buss: This work supported in part by Simons Foundation grant 578919. Anupam Das: This work was supported by a Marie Sk{\l}odowska-Curie fellowship, Monotonicity in Logic and Complexity, ERC project 753431. Publisher Copyright: {\textcopyright} Sam Buss, Anupam Das, and Alexander Knop.; 28th EACSL Annual Conference on Computer Science Logic (CSL 2020) ; Conference date: 13-01-2020 Through 16-01-2020",

year = "2020",

month = jan,

day = "6",

doi = "10.4230/LIPIcs.CSL.2020.12",

language = "English",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl",

editor = "Maribel Fernandez and Anca Muscholl",

booktitle = "28th EACSL Annual Conference on Computer Science Logic (CSL 2020)",

address = "Germany",

}

Buss, S, Das, A & Knop, A 2020, Proof complexity of systems of (non-deterministic) decision trees and branching programs. in M Fernandez & A Muscholl (eds), 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)., 12, Leibniz International Proceedings in Informatics (LIPIcs), vol. 152, Schloss Dagstuhl, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), Barcelona, Spain, 13/01/20. https://doi.org/10.4230/LIPIcs.CSL.2020.12

Proof complexity of systems of (non-deterministic) decision trees and branching programs. / Buss, Sam; Das, Anupam; Knop, Alexander.
28th EACSL Annual Conference on Computer Science Logic (CSL 2020). ed. / Maribel Fernandez; Anca Muscholl. Schloss Dagstuhl, 2020. 12 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 152).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Buss, Sam

AU - Das, Anupam

AU - Knop, Alexander

N1 - Funding Information: Funding Sam Buss: This work supported in part by Simons Foundation grant 578919. Anupam Das: This work was supported by a Marie Skłodowska-Curie fellowship, Monotonicity in Logic and Complexity, ERC project 753431. Publisher Copyright: © Sam Buss, Anupam Das, and Alexander Knop.

PY - 2020/1/6

Y1 - 2020/1/6

N2 - 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.

AB - 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.

KW - proof complexity

KW - decision trees

KW - branching programs

KW - logspace

KW - sequent calculus

KW - non-determinism

KW - low-depth complexity

UR - http://www.scopus.com/inward/record.url?scp=85077973046&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.CSL.2020.12

DO - 10.4230/LIPIcs.CSL.2020.12

M3 - Conference contribution

AN - SCOPUS:85077973046

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

BT - 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

A2 - Fernandez, Maribel

A2 - Muscholl, Anca

PB - Schloss Dagstuhl

T2 - 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Y2 - 13 January 2020 through 16 January 2020

ER -

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

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this