Recherche et construction de preuves en logique non-commutative - Université de Lorraine Accéder directement au contenu
Thèse Année : 2004

Recherche et construction de preuves en logique non-commutative

Résumé

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.
La logique NL étend la logique linéaire en y ajoutant des connecteurs non-commutatifs. Sa particularité vient des interactions entre les connecteurs commutatifs et non-commutatifs. Une première étude nous a conduit à analyser ces interactions dans le cadre des réseaux de preuve. Leur prise en compte lors de la recherche de preuves par composition (construction) nécessite l'introduction de structures spécifiques (labels, graphes de dépendances). Nous proposons ainsi plusieurs algorithmes de construction de réseaux de preuve pour le fragment multiplicatif de NL. Une autre approche étudiée est celle de la recherche de preuves par décomposition, mise en oeuvre en particulier dans le cadre des méthodes des connexions. En utilisant des labels associés aux sous-formules, et des contraintes exprimées sur ces labels, nous proposons une caractérisation par les connexions pour MNL. La méthode des connexions associée peut être vue comme un nouvel algorithme de construction de réseaux de preuve.
Fichier non déposé

Dates et versions

tel-01746753 , version 1 (29-03-2018)

Identifiants

  • HAL Id : tel-01746753 , version 1

Accès intranet

Citer

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⟩
29 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More