Connection-based proof construction in Non-Commutative Logic

Didier Galmiche 1 Jean-Marc Notin 1
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We propose a connection-based characterization of the multiplicative fragment of non-commutative logic (MNL), that is a conservative extension of both commutative (MLL) and non-commutative or cyclic (MCyLL) linear logic. It is based on a characterization for MLL together with the introduction of labels and constraints from a formula polarization process. We also study a similar characterization for the intuitionistic fragment of MNL. Finally, we consider the relationships between these results and proof nets construction in MNL based on labels and constraints.
Mots-clés : logique lineaire constraints linear logic non-commutative logic connection method labels logique non-commutative methode des connexions contraintes
Type de document :
Communication dans un congrès
Moshe Y. Vardi and Andrei Voronkov. 10th International Conference on Logic for Programming Artificial Intelligence and Reasoning 2003 - LPAR'03, 2003, Almaty/Kazakhstan, Springer Verlag, 2850, pp.422 - 436, 2003, Lecture Notes in Computer Science. 〈10.1007/b13986〉
Liste complète des métadonnées
https://hal.inria.fr/inria-00099554
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:38:40
Dernière modification le : mardi 24 avril 2018 - 13:34:49

Lien texte intégral

openaccess

Identifiants

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

Didier Galmiche, Jean-Marc Notin. Connection-based proof construction in Non-Commutative Logic. Moshe Y. Vardi and Andrei Voronkov. 10th International Conference on Logic for Programming Artificial Intelligence and Reasoning 2003 - LPAR'03, 2003, Almaty/Kazakhstan, Springer Verlag, 2850, pp.422 - 436, 2003, Lecture Notes in Computer Science. 〈10.1007/b13986〉. 〈inria-00099554〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

130

Contact


archive-ouverte@inria.fr