Sémantique des phases, réseaux de preuve et divers problèmes de décision en logique linéaire.

Linear logic (LL) is very expressive: the smallest propositonal fragment is already NP-complete and the whole logic is indecidable. One can simulate usual computational models as many counters machines. The decidability of the fragment multiplicative exponential LL (MELL) is an open problem. This thesis establishes a correctness result for semi-linear phase semantics from the proof of the decidability of the accessibility in Petri nets. Indeed, the provability in some Horn fragment of MELL corresponds to this decision problem in the Petri nets. This result is a first step towards the decidability of MELL fragment (Y.Lafont conjecture). The next chapter describes an encoding of the hamiltonian circuits problem into the multiplicative LL (MLL). In this graph-theoretical problem, the additive notion of choice is viewed multiplicatively. This procedure may be used for other combinatorial problems. We obtain a new proof of the NP-completeness of MLL. M.Kanovich has established this result in 1992 using a reduction to 3-partition problem. But this reduction can not be used for the study of purely non-commutative fragment of MLL (this open problem needs another encoding). This is a joined work with T.Krantz. Finally we give a quadratic time correctness criterion for the proof nets of the non-commutative logic of P.Ruet. This logic contains LL and cyclic linear logic. Moreover we handle the case of proof nets with cuts.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