From Deep Inference to Proof Nets

Lutz Straßburger 1, 2
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : This paper shows how derivations in (a variation of) SKS can be translated into proof nets. Since an SKS derivation contains more information about a proof than the corresponding proof net, we observe a loss of information which can be understood as ``eliminating bureaucracy''. Technically this is achieved by cut reduction on proof nets. As an intermediate step between the two extremes, SKS derivations and proof nets, we will see nets representing derivations in ``Formalism A''.
Type de document :
Communication dans un congrès
Structures and Deduction 2005 (ICALP Workshop), Jul 2005, Lisbon, Portugal, 2005
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00130501
Contributeur : Lutz Straßburger <>
Soumis le : lundi 12 février 2007 - 15:49:14
Dernière modification le : jeudi 10 mai 2018 - 02:06:34
Document(s) archivé(s) le : mardi 6 avril 2010 - 21:07:04

Fichier

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

Identifiants

  • HAL Id : inria-00130501, version 1

Collections

Citation

Lutz Straßburger. From Deep Inference to Proof Nets. Structures and Deduction 2005 (ICALP Workshop), Jul 2005, Lisbon, Portugal, 2005. 〈inria-00130501〉

Partager

Métriques

Consultations de la notice

221

Téléchargements de fichiers

117