| HAL-Inria | Publications, software ... of Inria's scientists |
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.
Cited literature [36 references]
https://hal.inria.fr/inria-00441213
Contributor : Alessio Guglielmi <>
Submitted on : Tuesday, December 15, 2009 - 10:51:38 AM
Last modification on : Friday, March 27, 2020 - 3:49:43 AM
Document(s) archivé(s) le : Thursday, June 17, 2010 - 11:41:26 PM
Contributor : Alessio Guglielmi <>
Submitted on : Tuesday, December 15, 2009 - 10:51:38 AM
Last modification on : Friday, March 27, 2020 - 3:49:43 AM
Document(s) archivé(s) le : Thursday, June 17, 2010 - 11:41:26 PM
File
QuasiPolNormDI.pdf
Files produced by the author(s)