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.

En logique classique, la formalisation du fonctionnement des réseaux de Petri (RdP) se heurte à la pérennité de la vérité. En logique modale, elle impose la construction préalable du graphe des marquages accessibles. A contrario, la logique linéaire (LL) fondée par Girard permet de formaliser directement par des séquents prouvables purement propositionnels les relations d'accessibilité dans les RdP : toute transition apparaît comme une implication linéaire disponible ad libitum entre les propositions traduisant ses marquages d'entrée et de sortie. Pour approfondir cette formalisation, nous définissons comme primitives en LL les notions de ressource, d'action et de consommabilité/productibilité, analogues mais distinctes de celles de proposition, de déduction et de vérité/fausseté en logique classique. Nous développons une interprétation concrète pour tous les connecteurs linéaires en cohérence avec leurs propriétés syntaxiques. Nous présentons le connecteur « par » comme un opérateur de cumul disjoint d'exemplaires de ressources (dual du connecteur « fois » de cumul conjoint) et la négation linéaire « nil » comme un inverseur du sens du temps. Cette concrétisation montre les limites des formalisations existantes des RdP en LL ; nous les généralisons en traduisant chaque transition par une implication linéaire ordinaire, traitée comme une ressource périssable, dont tout exemplaire consommé correspond à une occurrence de franchissement. Ainsi, nous apportons une expression logique aux aspects primordiaux du fonctionnement des RdP : nous démontrons qu'une relation d'accessibilité par séquence de transitions équivaut à un séquent prouvable et que l'équation fondamentale est l'expression algébrique d'un corollaire du critère d'équilibrage en LL. Grâce à la combinatoire de tous les connecteurs linéaires, notre approche ouvre des perspectives d'analyse de relations complexes d'accessibilité comme celles de reprise après défa illance dans un système industriel.