Quasipolynomial normalisation in deep inference via atomic flows and threshold formulae

Alessio Guglielmi, Paola Bruscoli, Tom Gundersen, Michel Parigot

Research output: Contribution to journalArticle

3 Citations (Scopus)
74 Downloads (Pure)

Abstract

Jeˇr´abek showed that cuts in classical propositional logic proofs in deep inference can be eliminated in quasipolynomial time. The proof is indirect and it relies on a result of Atserias, Galesi and Pudl´ak about monotone sequent calculus and a correspondence
between that system and cut-free deep-inference proofs. In this paper we give a direct proof of Jeˇr´abek’s result: we give a quasipolynomial-time cut-elimination procedure for classical
propositional logic in deep inference. The main new ingredient is the use of a computational trace of deep-inference proofs called atomic flows, which are both very simple (they only trace structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination procedure.
Original languageEnglish
Article number5
Pages (from-to)1-30
Number of pages30
JournalLogical Methods in Computer Science
Volume12
Issue number2
DOIs
Publication statusPublished - 3 May 2016

Cite this

Quasipolynomial normalisation in deep inference via atomic flows and threshold formulae. / Guglielmi, Alessio; Bruscoli, Paola; Gundersen, Tom; Parigot, Michel.

In: Logical Methods in Computer Science, Vol. 12, No. 2, 5, 03.05.2016, p. 1-30.

Research output: Contribution to journalArticle

@article{4ba73f3bad8b46a38984804329bed24f,
title = "Quasipolynomial normalisation in deep inference via atomic flows and threshold formulae",
abstract = "Jeˇr´abek showed that cuts in classical propositional logic proofs in deep inference can be eliminated in quasipolynomial time. The proof is indirect and it relies on a result of Atserias, Galesi and Pudl´ak about monotone sequent calculus and a correspondencebetween that system and cut-free deep-inference proofs. In this paper we give a direct proof of Jeˇr´abek’s result: we give a quasipolynomial-time cut-elimination procedure for classicalpropositional logic in deep inference. The main new ingredient is the use of a computational trace of deep-inference proofs called atomic flows, which are both very simple (they only trace structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination procedure.",
author = "Alessio Guglielmi and Paola Bruscoli and Tom Gundersen and Michel Parigot",
year = "2016",
month = "5",
day = "3",
doi = "10.2168/LMCS-12(2:5)2016",
language = "English",
volume = "12",
pages = "1--30",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "Technischen Universitat Braunschweig",
number = "2",

}

TY - JOUR

T1 - Quasipolynomial normalisation in deep inference via atomic flows and threshold formulae

AU - Guglielmi, Alessio

AU - Bruscoli, Paola

AU - Gundersen, Tom

AU - Parigot, Michel

PY - 2016/5/3

Y1 - 2016/5/3

N2 - Jeˇr´abek showed that cuts in classical propositional logic proofs in deep inference can be eliminated in quasipolynomial time. The proof is indirect and it relies on a result of Atserias, Galesi and Pudl´ak about monotone sequent calculus and a correspondencebetween that system and cut-free deep-inference proofs. In this paper we give a direct proof of Jeˇr´abek’s result: we give a quasipolynomial-time cut-elimination procedure for classicalpropositional logic in deep inference. The main new ingredient is the use of a computational trace of deep-inference proofs called atomic flows, which are both very simple (they only trace structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination procedure.

AB - Jeˇr´abek showed that cuts in classical propositional logic proofs in deep inference can be eliminated in quasipolynomial time. The proof is indirect and it relies on a result of Atserias, Galesi and Pudl´ak about monotone sequent calculus and a correspondencebetween that system and cut-free deep-inference proofs. In this paper we give a direct proof of Jeˇr´abek’s result: we give a quasipolynomial-time cut-elimination procedure for classicalpropositional logic in deep inference. The main new ingredient is the use of a computational trace of deep-inference proofs called atomic flows, which are both very simple (they only trace structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination procedure.

U2 - 10.2168/LMCS-12(2:5)2016

DO - 10.2168/LMCS-12(2:5)2016

M3 - Article

VL - 12

SP - 1

EP - 30

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 2

M1 - 5

ER -