Proof nets for first-order additive linear logic

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 : mercredi 14 novembre 2018 - 16:14:01

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

138

Téléchargements de fichiers

32