Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae

Paola Bruscoli (1) , Alessio Guglielmi (1) , Tom Gundersen (2) , Michel Parigot (3)

1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
2 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
3 PPS - Preuves, Programmes et Systèmes

Jerábek showed that analytic propositional-logic deep-inference proofs can be constructed in quasipolynomial time from nonanalytic proofs. In this work, we improve on that as follows: 1) we significantly simplify the technique; 2) our normalisation procedure is direct, i.e., it is internal to deep inference. The paper is self-contained, and provides a starting point and a good deal of information for tackling the problem of whether a polynomial-time normalisation procedure exists.

Domaines: Complexité [cs.CC]

Paola Bruscoli, Alessio Guglielmi, Tom Gundersen, Michel Parigot. Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae. 2009. ⟨inria-00441213⟩