Soutenance de thèse d'Ivan Noyer

Bonjour,

J'ai le plaisir de vous inviter à la soutenance de ma thèse intitulée :

" Trois études sur l'implantation des matrices en FoCaLiZe, les
preuves quantitatives et la
réutilisation de preuves"

qui aura lieu le 28 septembre à 10h, campus de Jussieu tour 25-26, salle 101.

Le jury sera composé de:
Directeur de thèse:
M. Renaud Rioboo (ENSIIE)

Rapporteurs:
M. Gilles Dowek (LIX)
M. Choukri-Bey Ben Yelles (IUT Valence)

Examinateurs:
Mme. Alessandra Carbone (CNRS-UPMC)
M. Jacques Carette (McMaster University)
M. Roberto Di Cosmo (PPS)
M. Claudio Sacerdotti Coen (University of Bologna)

Résumé :

L'environnement de développement sûr FoCaLize
(http://focalize.inria.fr/) permet l'écriture de spécifications,
l'implantation de méthodes et l'écriture de la preuve de l'adéquation
d'un code à sa spécification.

Cette thèse part de la volonté d'implanter une bibliothèque de
matrices dans FoCaLize. Nous proposons une spécification dans laquelle
toutes les matrices sur un même anneau commutatif unitaire sont vues
comme des éléments d'une algèbre unitaire unique. Dans un tel
contexte, les opérateurs d'addition et de multiplication sont des
fonctions totales. Cela permet de les coder par des méthodes
récursives dans un type de données ne tenant pas compte de la
dimension des matrices.

Nous nous sommes ensuite intéressés au problème de la
recherche de spécifications dans la bibiothèque FoCaLize, laquelle est
considérée comme une base de données de formules du premier ordre
(prouvées ou non). La recherche d'une spécification aboutit s'il
existe une formule de la bibliothèque dont l'information cherchée soit
une conséquence dans un certain fragment de la logique du premier
ordre. Ce fragment est celui des preuves dites "quantitatives". Ces
dernières sont des preuves n'utilisant que les règles de
quantification du calcul des séquents et se terminant par la règle
axiome. Nous établissons un critère nécessaire et suffisant pour la
réussite de notre recherche, retrouvant ainsi un résultat connu. Nous
donnons deux formalisations équivalentes de notre critère. Nous
caractérisons ensuite l'admissibilité de la règle de coupure dans
notre fragment de la logique par une méthode que nous pensons originale.

Dans la foulée nous mettons en évidence une condition
nécessaire et suffisante pour qu'une modification des symboles
fonctionnels et relationnels dans un séquent du premier ordre permette
d'obtenir un nouveau séquent possédant une preuve quantitative. Nous
utilisons ce résultat pour proposer une méthode de réutilisation de
preuve par analogie dans la lignée de travaux antérieurs.

Finalement, nous décrivons informellement comment utiliser ces
résultats concernant la logique du premier dans le cadre de
l'environnement FoCaLiZe.