Deep inference and expansion trees for second-order multiplicative linear logic - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Mathematical Structures in Computer Science Année : 2019

Deep inference and expansion trees for second-order multiplicative linear logic

Résumé

In this paper, we introduce the notion of expansion tree for linear logic. As in Miller's original work, we have a shallow reading of an expansion tree that corresponds to the conclusion of the proof, and a deep reading which is a formula that can be proved by propositional rules. We focus our attention to MLL2, and we also present a deep inference system for that logic. This allows us to give a syntactic proof to a version of Herbrand's theorem.
Fichier principal
Vignette du fichier
ExpTreesLL.pdf (325.89 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-01942410 , version 1 (03-12-2018)

Identifiants

Citer

Lutz Strassburger. Deep inference and expansion trees for second-order multiplicative linear logic. Mathematical Structures in Computer Science, 2019, Special Issue 8 (A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller’s 60th birthday), 29, pp.1030-1060. ⟨10.1017/S0960129518000385⟩. ⟨hal-01942410⟩
81 Consultations
229 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More