A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae

Paola Bruscoli; Alessio Guglielmi; Tom Gundersen; Michel Parigot

doi:10.1007/978-3-642-17511-4_9

A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae

Paola Bruscoli, Alessio Guglielmi, Tom Gundersen, Michel Parigot

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

11 Citations (SciVal)

151 Downloads (Pure)

Abstract

Jeřábek showed in 2008 that cuts in propositional-logic deep-inference proofs can be eliminated in quasipolynomial time. The proof is an indirect one relying on a result of Atserias, Galesi and Pudlák about monotone sequent calculus and a correspondence between this system and cut-free deep-inference proofs. In this paper we give a direct proof of Jeřábek’s result: we give a quasipolynomial-time cut-elimination procedure in propositional-logic 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 trace only structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination.

Original language	English
Title of host publication	Logic for programming, artificial intelligence, and reasoning: 16th International Conference, LPAR-16, Dakar, Senegal, April 25–May 1, 2010, revised selected papers
Editors	E M Clarke, A Voronkov
Place of Publication	Berlin
Publisher	Springer
Pages	136-153
Number of pages	18
ISBN (Electronic)	9783642175114
ISBN (Print)	9783642175107
DOIs	https://doi.org/10.1007/978-3-642-17511-4_9
Publication status	Published - 2010

Publication series

Name	Lecture Notes in Computer Science
Volume	6355
ISSN (Print)	0302-9743

Access to Document

10.1007/978-3-642-17511-4_9

Author's version
The original publication is available at www.springerlink.com
Accepted author manuscript, 407 KB

Cite this

Bruscoli, P., Guglielmi, A., Gundersen, T., & Parigot, M. (2010). A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae. In E. M. Clarke, & A. Voronkov (Eds.), Logic for programming, artificial intelligence, and reasoning: 16th International Conference, LPAR-16, Dakar, Senegal, April 25–May 1, 2010, revised selected papers (pp. 136-153). (Lecture Notes in Computer Science; Vol. 6355). Springer. https://doi.org/10.1007/978-3-642-17511-4_9

A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae. / Bruscoli, Paola; Guglielmi, Alessio; Gundersen, Tom et al.
Logic for programming, artificial intelligence, and reasoning: 16th International Conference, LPAR-16, Dakar, Senegal, April 25–May 1, 2010, revised selected papers. ed. / E M Clarke; A Voronkov. Berlin: Springer, 2010. p. 136-153 (Lecture Notes in Computer Science; Vol. 6355).

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

Bruscoli, P, Guglielmi, A, Gundersen, T & Parigot, M 2010, A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae. in EM Clarke & A Voronkov (eds), Logic for programming, artificial intelligence, and reasoning: 16th International Conference, LPAR-16, Dakar, Senegal, April 25–May 1, 2010, revised selected papers. Lecture Notes in Computer Science, vol. 6355, Springer, Berlin, pp. 136-153. https://doi.org/10.1007/978-3-642-17511-4_9

Bruscoli P, Guglielmi A, Gundersen T, Parigot M. A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae. In Clarke EM, Voronkov A, editors, Logic for programming, artificial intelligence, and reasoning: 16th International Conference, LPAR-16, Dakar, Senegal, April 25–May 1, 2010, revised selected papers. Berlin: Springer. 2010. p. 136-153. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-17511-4_9

Bruscoli, Paola ; Guglielmi, Alessio ; Gundersen, Tom et al. / A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae. Logic for programming, artificial intelligence, and reasoning: 16th International Conference, LPAR-16, Dakar, Senegal, April 25–May 1, 2010, revised selected papers. editor / E M Clarke ; A Voronkov. Berlin : Springer, 2010. pp. 136-153 (Lecture Notes in Computer Science).

@inproceedings{5ace1776890445149f31bb1ad71f0705,

title = "A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae",

abstract = "Je{\v r}{\'a}bek showed in 2008 that cuts in propositional-logic deep-inference proofs can be eliminated in quasipolynomial time. The proof is an indirect one relying on a result of Atserias, Galesi and Pudl{\'a}k about monotone sequent calculus and a correspondence between this system and cut-free deep-inference proofs. In this paper we give a direct proof of Je{\v r}{\'a}bek{\textquoteright}s result: we give a quasipolynomial-time cut-elimination procedure in propositional-logic 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 trace only structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination.",

author = "Paola Bruscoli and Alessio Guglielmi and Tom Gundersen and Michel Parigot",

year = "2010",

doi = "10.1007/978-3-642-17511-4_9",

language = "English",

isbn = "9783642175107",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "136--153",

editor = "Clarke, {E M } and Voronkov, {A }",

booktitle = "Logic for programming, artificial intelligence, and reasoning: 16th International Conference, LPAR-16, Dakar, Senegal, April 25–May 1, 2010, revised selected papers",

}

TY - GEN

T1 - A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae

AU - Bruscoli, Paola

AU - Guglielmi, Alessio

AU - Gundersen, Tom

AU - Parigot, Michel

PY - 2010

Y1 - 2010

N2 - Jeřábek showed in 2008 that cuts in propositional-logic deep-inference proofs can be eliminated in quasipolynomial time. The proof is an indirect one relying on a result of Atserias, Galesi and Pudlák about monotone sequent calculus and a correspondence between this system and cut-free deep-inference proofs. In this paper we give a direct proof of Jeřábek’s result: we give a quasipolynomial-time cut-elimination procedure in propositional-logic 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 trace only structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination.

AB - Jeřábek showed in 2008 that cuts in propositional-logic deep-inference proofs can be eliminated in quasipolynomial time. The proof is an indirect one relying on a result of Atserias, Galesi and Pudlák about monotone sequent calculus and a correspondence between this system and cut-free deep-inference proofs. In this paper we give a direct proof of Jeřábek’s result: we give a quasipolynomial-time cut-elimination procedure in propositional-logic 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 trace only structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination.

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

UR - http://arxiv.org/abs/0903.5392v1

UR - http://dx.doi.org/10.1007/978-3-642-17511-4_9

U2 - 10.1007/978-3-642-17511-4_9

DO - 10.1007/978-3-642-17511-4_9

M3 - Chapter in a published conference proceeding

SN - 9783642175107

T3 - Lecture Notes in Computer Science

SP - 136

EP - 153

BT - Logic for programming, artificial intelligence, and reasoning: 16th International Conference, LPAR-16, Dakar, Senegal, April 25–May 1, 2010, revised selected papers

A2 - Clarke, E M

A2 - Voronkov, A

PB - Springer

CY - Berlin

ER -

A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae

Abstract

Publication series

Access to Document

Other files and links

Fingerprint

COMPLEXITY AND NON-DETERMINISM IN DEEP INFERENCE

Cite this

A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae

Abstract

Publication series

Access to Document

Other files and links

Fingerprint

Projects

COMPLEXITY AND NON-DETERMINISM IN DEEP INFERENCE

Cite this