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.

2006-2010 Publications

• 2010
  • Y. Noyer : “Trois études sur l’implantation des matrices en FoCaLiZe, les preuves quantitatives et la réutilisation de preuves”, thesis, phd defence 09/28/2010, supervision Rioboo, Renaud (2010)
• 2009
  • I. Noyer, R. Rioboo : “Reusing Proofs in a Mathematical Library”, Calculemus 2009 - 16^th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Ontario, Canada (2009)
• 2006
  • I. Noyer, R. Rioboo : “Mechanized Calculus and Algebra: the FoCaL approach”, Second International Congress on Mathematical Software ICMS'2006, Castro Urdiales, Spain (2006)