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

Lutz Straßburger 1, 2, 3
Abstract : 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.
Type de document :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2018, pp.1-31. 〈10.1017/S0960129518000385〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01942410
Contributeur : Lutz Straßburger <>
Soumis le : lundi 3 décembre 2018 - 11:08:55
Dernière modification le : mercredi 5 décembre 2018 - 01:14:25

Fichier

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

Identifiants

Citation

Lutz Straßburger. Deep inference and expansion trees for second-order multiplicative linear logic. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2018, pp.1-31. 〈10.1017/S0960129518000385〉. 〈hal-01942410〉

Partager

Métriques

Consultations de la notice

27

Téléchargements de fichiers

9