some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

   Volume 1 (2005)

   Volume 2 (2006)

   Volume 3 (2007)

   Volume 4 (2008)

   Volume 5 (2009)

   Volume 6 (2010)

   Volume 7 (2011)

   Volume 8 (2012)

   Volume 9 (2013)

   Volume 10 (2014)

   Volume 11 (2015)

   Volume 12 (2016)

      Issue 1

      Issue 2

      Issue 3

      Issue 4

   Volume 13 (2017)

SPECIAL ISSUES

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

VOLUME 12, ISSUE 2, PAPER 5


Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae

©Paola Bruscoli, University of Bath
©Alessio Guglielmi, University of Bath
©Tom Gundersen, Red Hat, Inc.
©Michel Parigot, Laboratoire PPS, UMR 7126, CNRS & Université Paris 7

Abstract
Jeřábek 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ák 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řábek'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.

Publication date: May 3, 2016

Full Text: PDF | PostScript
DOI: 10.2168/LMCS-12(2:5)2016

Hit Counts: 1957

Creative Commons