Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae

Abstract : 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.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

Cited literature [36 references]  Display  Hide  Download

https://hal.inria.fr/inria-00441213
Contributor : Alessio Guglielmi <>
Submitted on : Tuesday, December 15, 2009 - 10:51:38 AM
Last modification on : Thursday, April 4, 2019 - 1:19:26 AM
Long-term archiving on : Thursday, June 17, 2010 - 11:41:26 PM

File

QuasiPolNormDI.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00441213, version 1

Citation

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

Share

Metrics

Record views

312

Files downloads

361