On the resolution semiring (sur le semi anneau de résolution)

Carte non disponible
Speaker Home page :
Speaker :
Speaker Affiliation :


Date(s) - 04/12/2014
9 h 30 min - 11 h 00 min


Soutenance de thèse

We study in this thesis a semiring structure with a product based on the resolution rule of logic programming.
This mathematical object was introduced initially in the setting of the geometry of interaction program in order to model the cut-elimination procedure of linear logic.
It provides us with an algebraic and abstract setting, while being presented in a syntactic and concrete way, in which a theoretical study of computation can be carried on.

We will review first the interactive interpretation of proof theory within this semiring via the categorical axiomatization of the geometry of interaction approach. This interpretation establishes a way to translate functional programs into a very simple form of logic programs.

Secondly, complexity theory problematics will be considered: while the nilpotency problem in the semiring we study is undecidable in general, it will appear that certain restrictions allow for characterizations of (deterministic and non-deterministic) logarithmic space and (deterministic) polynomial time computation.

*Membres du jury :

Pierre-Louis Curien
Jean-Yves Girard (directeur de thèse)
Ugo dal Lago (rapporteur)
Paul-André Melliès
Myriam Quatrini
Ulrich Schöpp
Philip Scott (rapporteur)
Kazushige Terui

Lien : theses.fr

Retour en haut 

Secured By miniOrange