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 :
File URL :
Complete list of metadatas
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 10:44:12 AM
Last modification on : Tuesday, September 1, 2020 - 3:19:55 PM


  • 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