On the proof complexity of cut-free bounded deep inference

Anupam Das

Research output: Chapter in Book/Report/Conference proceedingChapter

7 Citations (Scopus)

Abstract

It has recently been shown that cut-free deep inference systems exhibit an exponential speed-up over cut-free sequent systems, in terms of proof size. While this is good for proof complexity, there remains the problem of typically high proof search non-determinism induced by the deep inference methodology: the higher the depth of inference, the higher the non-determinism. In this work we improve on the proof search side by demonstrating that, for propositional logic, the same exponential speed-up in proof size can be obtained in bounded-depth cut-free systems. These systems retain the top-down symmetry of deep inference, but can otherwise be designed at the same depth level of sequent systems. As a result the non-determinism arising from the choice of rules at each stage of a proof is smaller than that of unbounded deep inference, while still giving access to the short proofs of deep inference.
Original languageEnglish
Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings
Place of PublicationHeidelberg
PublisherSpringer
Pages134-148
Number of pages15
Volume6793 LNAI
ISBN (Print)03029743
DOIs
Publication statusPublished - 2011
Event20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011, July 4, 2011 - July 8, 2011 - Bern, Switzerland
Duration: 1 Jan 2011 → …

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag

Conference

Conference20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011, July 4, 2011 - July 8, 2011
CountrySwitzerland
CityBern
Period1/01/11 → …

Cite this

Das, A. (2011). On the proof complexity of cut-free bounded deep inference. In Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings (Vol. 6793 LNAI, pp. 134-148). (Lecture Notes in Computer Science). Heidelberg: Springer. https://doi.org/10.1007/978-3-642-22119-4_12

On the proof complexity of cut-free bounded deep inference. / Das, Anupam.

Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings. Vol. 6793 LNAI Heidelberg : Springer, 2011. p. 134-148 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceedingChapter

Das, A 2011, On the proof complexity of cut-free bounded deep inference. in Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings. vol. 6793 LNAI, Lecture Notes in Computer Science, Springer, Heidelberg, pp. 134-148, 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011, July 4, 2011 - July 8, 2011, Bern, Switzerland, 1/01/11. https://doi.org/10.1007/978-3-642-22119-4_12
Das A. On the proof complexity of cut-free bounded deep inference. In Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings. Vol. 6793 LNAI. Heidelberg: Springer. 2011. p. 134-148. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-22119-4_12
Das, Anupam. / On the proof complexity of cut-free bounded deep inference. Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings. Vol. 6793 LNAI Heidelberg : Springer, 2011. pp. 134-148 (Lecture Notes in Computer Science).
@inbook{d9553a93253b4f378a4a8ed62e422b56,
title = "On the proof complexity of cut-free bounded deep inference",
abstract = "It has recently been shown that cut-free deep inference systems exhibit an exponential speed-up over cut-free sequent systems, in terms of proof size. While this is good for proof complexity, there remains the problem of typically high proof search non-determinism induced by the deep inference methodology: the higher the depth of inference, the higher the non-determinism. In this work we improve on the proof search side by demonstrating that, for propositional logic, the same exponential speed-up in proof size can be obtained in bounded-depth cut-free systems. These systems retain the top-down symmetry of deep inference, but can otherwise be designed at the same depth level of sequent systems. As a result the non-determinism arising from the choice of rules at each stage of a proof is smaller than that of unbounded deep inference, while still giving access to the short proofs of deep inference.",
author = "Anupam Das",
year = "2011",
doi = "10.1007/978-3-642-22119-4_12",
language = "English",
isbn = "03029743",
volume = "6793 LNAI",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "134--148",
booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings",

}

TY - CHAP

T1 - On the proof complexity of cut-free bounded deep inference

AU - Das, Anupam

PY - 2011

Y1 - 2011

N2 - It has recently been shown that cut-free deep inference systems exhibit an exponential speed-up over cut-free sequent systems, in terms of proof size. While this is good for proof complexity, there remains the problem of typically high proof search non-determinism induced by the deep inference methodology: the higher the depth of inference, the higher the non-determinism. In this work we improve on the proof search side by demonstrating that, for propositional logic, the same exponential speed-up in proof size can be obtained in bounded-depth cut-free systems. These systems retain the top-down symmetry of deep inference, but can otherwise be designed at the same depth level of sequent systems. As a result the non-determinism arising from the choice of rules at each stage of a proof is smaller than that of unbounded deep inference, while still giving access to the short proofs of deep inference.

AB - It has recently been shown that cut-free deep inference systems exhibit an exponential speed-up over cut-free sequent systems, in terms of proof size. While this is good for proof complexity, there remains the problem of typically high proof search non-determinism induced by the deep inference methodology: the higher the depth of inference, the higher the non-determinism. In this work we improve on the proof search side by demonstrating that, for propositional logic, the same exponential speed-up in proof size can be obtained in bounded-depth cut-free systems. These systems retain the top-down symmetry of deep inference, but can otherwise be designed at the same depth level of sequent systems. As a result the non-determinism arising from the choice of rules at each stage of a proof is smaller than that of unbounded deep inference, while still giving access to the short proofs of deep inference.

UR - http://dx.doi.org/10.1007/978-3-642-22119-4_12

U2 - 10.1007/978-3-642-22119-4_12

DO - 10.1007/978-3-642-22119-4_12

M3 - Chapter

SN - 03029743

VL - 6793 LNAI

T3 - Lecture Notes in Computer Science

SP - 134

EP - 148

BT - Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings

PB - Springer

CY - Heidelberg

ER -