Deep Inference, Expansion Trees, and Proof Graphs for Second Order Propositional Multiplicative Linear Logic

Lutz Straßburger 1
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
Résumé : Dans cet article, nous introduisons la notion d’arbre d’expansion pour la logique linéaire. Comme dans le travail original de Miller, nous d définissons la formule extérieure d’un arbre d’expansion qui correspond à la conclusion de la preuve et la formule intérieure qui peut-être prouvée par des règles propositionnelles. Nous concentrons notre attentionsur MLL2 et nous présentons également un système d’inférence profonde pour cette logique. Cela nous permet de donner une preuve syntaxique d’une version du théorème de Herbrand.
Type de document :
Rapport
[Research Report] RR-9071, Inria Saclay Ile de France. 2017, pp.38
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01526831
Contributeur : Lutz Straßburger <>
Soumis le : mardi 23 mai 2017 - 15:34:21
Dernière modification le : mercredi 25 avril 2018 - 10:45:27
Document(s) archivé(s) le : vendredi 25 août 2017 - 00:47:14

Fichier

RR-9071.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01526831, version 1

Citation

Lutz Straßburger. Deep Inference, Expansion Trees, and Proof Graphs for Second Order Propositional Multiplicative Linear Logic. [Research Report] RR-9071, Inria Saclay Ile de France. 2017, pp.38. 〈hal-01526831〉

Partager

Métriques

Consultations de la notice

149

Téléchargements de fichiers

62