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.
Type de document :
Pré-publication, Document de travail
2009
Liste complète des métadonnées

Littérature citée [36 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00441213
Contributeur : Alessio Guglielmi <>
Soumis le : mardi 15 décembre 2009 - 10:51:38
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48
Document(s) archivé(s) le : jeudi 17 juin 2010 - 23:41:26

Fichier

QuasiPolNormDI.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00441213, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

225

Téléchargements de fichiers

145