Skip to Main content Skip to Navigation

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
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
3 PPS - Preuves, Programmes et Systèmes
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 : Friday, March 27, 2020 - 3:49:43 AM
Document(s) archivé(s) le : Thursday, June 17, 2010 - 11:41:26 PM

File

Vignette du document
QuasiPolNormDI.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00441213, version 1

Collections

CNRS | INRIA | LIX | X | X-LIX | PPS | LORIA | UNIV-LORRAINE | X-DEP-INFO | UNIV-PARIS7 | USPC

Citation

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

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

327

Files downloads

432

 

Contact                    Legal Notice                    Personal Data