Bruscoli, Paola and Guglielmi, Alessio and Gundersen, Tom and Parigot, Michel - Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae

lmcs:1637 - Logical Methods in Computer Science, May 3, 2016, Volume 12, Issue 2
Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae

Authors: Bruscoli, Paola and Guglielmi, Alessio and Gundersen, Tom and Parigot, Michel

Je\v{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\v{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.


Source : oai:arXiv.org:0903.5392
DOI : 10.2168/LMCS-12(2:5)2016
Volume: Volume 12, Issue 2
Published on: May 3, 2016
Submitted on: April 29, 2014
Keywords: Computer Science - Computational Complexity,Computer Science - Logic in Computer Science,F.4.1,F.2.2


Share

Consultation statistics

This page has been seen 106 times.
This article's PDF has been downloaded 76 times.