Showing 1–1 of 1 results for author: Parigot, M

Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae

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

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-ti… ▽ More 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. △ Less

Submitted 2 May, 2016; v1 submitted 31 March, 2009; originally announced March 2009.

Comments: Accepted by Logical Methods in Computer Science

ACM Class: F.4.1; F.2.2

Journal ref: Logical Methods in Computer Science, Volume 12, Issue 2 (May 3, 2016) lmcs:1637