Quasipolynomial normalisation in deep inference via atomic flows and threshold formulae

Alessio Guglielmi, Paola Bruscoli, Tom Gundersen, Michel Parigot

Research output: Contribution to journalArticlepeer-review

5 Citations (SciVal)
80 Downloads (Pure)


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
Issue number2
Early online date3 May 2016
Publication statusPublished - 31 Dec 2016


Dive into the research topics of 'Quasipolynomial normalisation in deep inference via atomic flows and threshold formulae'. Together they form a unique fingerprint.

Cite this