Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae

• Published in: Logical Methods in Computer Science
• Main Authors: Paola Bruscoli, Alessio Guglielmi, Tom Gundersen, Michel Parigot
• Format: Article
• Language: English
• Published: Logical Methods in Computer Science e.V. 2016-05-01
• Subjects: computer science - computational complexity; computer science - logic in computer science; f.4.1; f.2.2
• Online Access: https://lmcs.episciences.org/1637/pdf

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.