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 proceedingChapter in a published conference proceeding

11 Citations (SciVal)
138 Downloads (Pure)


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 languageEnglish
Title of host publicationLogic for programming, artificial intelligence, and reasoning: 16th International Conference, LPAR-16, Dakar, Senegal, April 25–May 1, 2010, revised selected papers
EditorsE M Clarke, A Voronkov
Place of PublicationBerlin
Number of pages18
ISBN (Electronic)9783642175114
ISBN (Print)9783642175107
Publication statusPublished - 2010

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743

Cite this