LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » News » PhD students

NOYER Yves

PhD graduated
Team : SPI
Departure date : 09/28/2010
Supervision : Renaud RIOBOO

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

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.
Defence : 09/28/2010 - 10h - Site Jussieu - Salle Jean-Louis Laurière - 25-26/101
Jury members :
M. Gilles Dowek (LIX) [Rapporteur]
M. Choukri-Bey Ben Yelles (IUT Valence) [Rapporteur]
M. Renaud Rioboo (ENSIIE)
Mme. Alessandra Carbone (CNRS-UPMC)
M. Jacques Carette (McMaster University)
M. Roberto Di Cosmo (PPS)
M. Claudio Sacerdotti Coen (University of Bologna)

2006-2010 Publications

 Mentions légales
Site map |