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

Carte non disponible

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

Catégories


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

Olivier CHABROL
Posts created 14

Articles similaires

Commencez à saisir votre recherche ci-dessus et pressez Entrée pour rechercher. ESC pour annuler.

Retour en haut
Secured By miniOrange