Ordered sequents and proof nets
Retoré, Christian
HAL, tel-00585634 / Harvested from HAL
Cette thèse présente un calcul des séquents pour la logique linéaire enrichie d'un connecteur non commutatif et autodual "précède" situé entre le "par" et le "tenseur". Il est défini pour des séquents dont les formules sont orientées par un ordre partiel. Un calcul de réseaux de démonstration quotientant ce calcul des séquents est défini en termes de graphes orientés. Ce calcul est doté d'une sémantique dénotationnelle dans les espaces cohérents, préservée par élimination des coupures, un processus convergent et confluent. Des résultats combinatoires nécessaires sur les ordres partiels et sur la structure des graphes de démonstrations sont établies ainsi que quelques propriétés du calcul commutatif avec la règle MIX.
Publié le : 1993-02-26
Classification:  logic,  proof theory,  linear logic,  graphs,  partial orders,  graphes,  logique linéaire,  logique,  théorie de la démonstration,  ordres partiels,  AMS 03F52, 03F07, 03F05,03G30, 03B47, 03B70, 05C70, 06A07,,  [MATH]Mathematics [math],  [MATH.MATH-LO]Mathematics [math]/Logic [math.LO],  [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
@article{tel-00585634,
     author = {Retor\'e, Christian},
     title = {Ordered sequents and proof nets},
     journal = {HAL},
     volume = {1993},
     number = {0},
     year = {1993},
     language = {fr},
     url = {http://dml.mathdoc.fr/item/tel-00585634}
}
Retoré, Christian. Ordered sequents and proof nets. HAL, Tome 1993 (1993) no. 0, . http://gdmltest.u-ga.fr/item/tel-00585634/