Skip to Main content Skip to Navigation

Recherche et construction de preuves en logique non-commutative

Abstract : Partially commutative logics allow to express properties mixing concurency and sequentiality. Thus, the logic NL extends linear logic with non-commutative connectives. The characteristic of NL comes from the interactions between commutative and non-commutative connectives. A first study led us to analyze these interactions within the framework of proof nets. Taking such interactions into account during top-down proof search (proof nets construction) requires the introduction of specific structures (labels, dependency sets). Thus, we propose several algorithms for building proof nets in the multiplicative fragment of NL (MNL). Another studied approach is bottom-up proof search, in particular within the framework of connection methods. By using labels associated with the subformulas, and constraints expressed on these labels, we propose a connection characterization for MNL. The associated connection method can be seen like a new algorithm for proof nets construction in MNL.
Document type :
Complete list of metadata
Contributor : Thèses UL Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 10:44:12 AM
Last modification on : Saturday, October 16, 2021 - 11:26:08 AM

Links full text


  • HAL Id : tel-01746753, version 1



Jean-Marc Notin. Recherche et construction de preuves en logique non-commutative. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2004. Français. ⟨NNT : 2004NAN10183⟩. ⟨tel-01746753⟩



Record views