La logique linéaire (LL) permet de prendre naturellement en compte la notion de ressource. Elle est ainsi très expressive : le plus petit fragment propositionnel est déjà NP-complet alors que le plus grand est indécidable car on peut y simuler les modèles de calculs usuels comme les machines à registres. La décidabilité du fragment multiplicatif exponentiel de LL (MELL) est un problème ouvert. Cette thèse établit la complétude de la sémantique des phases semi-linéaire pour le fragment de Horn de MELL. La prouvabilité dans ce dernier est équivalente à l'accessibilité dans les réseaux de Pétri. Ce résultat constitue une première étape vers l'éventuelle décidabilité de MELL (conjecture de Y.Lafont). Le chapitre suivant développe le codage du problème des circuits hamiltoniens où la notion de choix (qui est ici naturellement traduite par les connecteurs additifs) est gérée multiplicativement. Ce procédé pourrait être étendu à l'étude d'autres problèmes de théorie des graphes. On obtient ainsi une nouvelle preuve de la NP-complétude du fragment multiplicatif de la logique linéaire. C'est un travail réalisé en commun avec T.Krantz. Enfin, on donne un critère de correction quadratique pour les réseaux de preuves de la logique non-commutative de P.Ruet (qui contient la logique linéaire et la logique linéaire cyclique). Il permet de plus de traiter les réseaux de preuve avec coupures.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00084344 |
| Date | 17 January 2001 |
| Creators | Mogbil, Virgile |
| Publisher | Université de la Méditerranée - Aix-Marseille II |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.002 seconds