Proof nets for first-order additive linear logic

Willem Heijltjes 1 Dominic Hughes 2 Lutz Straßburger 3, 4
3 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é : Nous présentons des réseaux de preuve canoniques pour la logique linéaire additive du premier ordre, le fragment de la logique linéaire avec somme, produit et quantificateurs du premier ordre. Nous présentons deux versions de nos réseaux de preuves. Pour l'un, réseaux à tmoin, conserve une information de témoin explicite à la quantification existentielle. Pour l'autre, réseaux d'unification, cette information est absente mais peut-être reconstruite par l'unification. Les réseaux d'unification incarnent une contribution centrale de l'article: les informations sur les témoins de premier ordre peuvent être implicites et reconstruites selon les besoins. Les réseaux à témoin sont canoniques pour le calcul des séquents additifs de premier ordre. Les réseaux d unification excluent en outre tout choix inessentiel pour les témoins existentiels. Les deux notions de réseau de preuve sont définies par la coalescence, un complément additif à la contractibilité multiplicative, et pour les réseaux de témoins, un critère supplémentaire de correction géométrique est fourni. Tous deux capturent l'élimination des coupures comme une opération de composition globale en une étape.
Type de document :
Rapport
[Research Report] RR-9201, Inria. 2018
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01867625
Contributeur : Lutz Straßburger <>
Soumis le : mardi 4 septembre 2018 - 14:40:35
Dernière modification le : mardi 2 octobre 2018 - 14:34:33

Fichier

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

Identifiants

  • HAL Id : hal-01867625, version 1

Citation

Willem Heijltjes, Dominic Hughes, Lutz Straßburger. Proof nets for first-order additive linear logic. [Research Report] RR-9201, Inria. 2018. 〈hal-01867625〉

Partager

Métriques

Consultations de la notice

134

Téléchargements de fichiers

32