Deep Inference, Expansion Trees, and Proof Graphs for Second Order Propositional Multiplicative Linear Logic - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2017

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

Inférence profonde, arbres d’expansion et graphes de preuves pour la logique linéaire multiplicative propositionelle du second ordre

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.
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.
Fichier principal
Vignette du fichier
RR-9071.pdf (680.34 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01526831 , version 1 (23-05-2017)

Identifiants

  • HAL Id : hal-01526831 , version 1

Citer

Lutz Strassburger. 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⟩
189 Consultations
149 Téléchargements

Partager

Gmail Facebook X LinkedIn More