Sur le Semi-anneau de Résolution

In this thesis, we study a semiring structure with a product based on theresolution rule of logic programming. This mathematical object was introducedinitially in the setting of the geometry of interaction program in order to modelthe cut-elimination procedure of linear logic. It provides us with an algebraicand abstract setting, while being presented in a syntactic and concrete way, inwhich a theoretical study of computation can be carried on.We will review first the interactive interpretation of proof theory withinthis semiring via the categorical axiomatization of the geometry of interactionapproach. This interpretation establishes a way to translate functional programsinto a very simple form of logic programs.Secondly, complexity theory problematics will be considered: while thenilpotency problem in the semiring we study is undecidable in general, it willappear that certain restrictions allow for characterizations of (deterministicand non-deterministic) logarithmic space and (deterministic) polynomial timecomputation.On étudie dans cette thèse une structure de semi-anneau dont le produit est basésur la règle de résolution de la programmation logique. Cet objet mathématiquea été initialement introduit dans le but de modéliser la procédure d’éliminationdes coupures de la logique linéaire, dans le cadre du programme de géométriede l’interaction. Il fournit un cadre algébrique et abstrait, tout en étant présentésous une forme syntaxique et concrète, dans lequel mener une étude théoriquedu calcul.On reviendra dans un premier temps sur l’interprétation interactive dela théorie de la démonstration dans ce semi-anneau, via l’axiomatisationcatégorique de l’approche de la géométrie de l’interaction. Cette interprétationétablit une traduction des programmes fonctionnels vers une forme très simplede programmes logiques.Dans un deuxième temps, on abordera des problématiques de théorie de lacomplexité: bien que le problème de la nilpotence dans le semi-anneau étudiésoit indécidable en général, on fera apparaître des restrictions qui permettent decaractériser le calcul en espace logarithmique (déterministe et non-déterministe)et en temps polynomial (déterministe)