A System of Interaction and Structure V: The Exponentials and Splitting

Alessio Guglielmi 1 Lutz Straßburger 2
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 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 : System NEL is the mixed commutative/non-commutative linear logic BV augmented with linear logic's exponentials, or, equivalently, it is MELL augmented with the non-commutative self-dual connective seq. System NEL is Turing-complete, it is able to directly express process algebra sequential composition and it faithfully models causal quantum evolution. In this paper, we show cut elimination for NEL, based on a property that we call splitting. NEL is presented in the calculus of structures, which is a deep-inference formalism, because no Gentzen formalism can express it analytically. The splitting theorem shows how and to what extent we can recover a sequent-like structure in NEL proofs. Together with the decomposition theorem, proved in the previous paper of the series, this immediately leads to a cut-elimination theorem for NEL.
Type de document :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2011, pp.1-22. 〈10.1017/S096012951100003X〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00441254
Contributeur : Lutz Straßburger <>
Soumis le : mercredi 28 janvier 2015 - 19:29:06
Dernière modification le : jeudi 10 mai 2018 - 02:06:59
Document(s) archivé(s) le : mercredi 29 avril 2015 - 11:36:08

Fichier

NEL-splitting.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Alessio Guglielmi, Lutz Straßburger. A System of Interaction and Structure V: The Exponentials and Splitting. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2011, pp.1-22. 〈10.1017/S096012951100003X〉. 〈inria-00441254v2〉

Partager

Métriques

Consultations de la notice

256

Téléchargements de fichiers

117