Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae

Paola Bruscoli, Alessio Guglielmi, Tom Gundersen +1

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 Ats…