Skip to Main content Skip to Navigation
Conference papers

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
Document type :
Conference papers
Complete list of metadata
https://hal.inria.fr/inria-00099554
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 9:38:40 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM

Identifiers

Collections

INRIA | CNRS | LORIA | UNIV-LORRAINE

Citation

Didier Galmiche, Jean-Marc Notin. Connection-based proof construction in Non-Commutative Logic. 10th International Conference on Logic for Programming Artificial Intelligence and Reasoning 2003 - LPAR'03, 2003, Almaty/Kazakhstan, pp.422 - 436, ⟨10.1007/b13986⟩. ⟨inria-00099554⟩

Export

BibTeX TEI DC DCterms EndNote Datacite

Share

Metrics

Record views

76

 

Contact                    Legal Notice                    Personal Data