Abstract FR:

Cette thèse part de la volonté d'implanter une bibliothèque de matrices dans l'environnement de développement sûr FoCaLize. Nous donnons 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 recherchons ensuite des spécifications dans la bibliothèque FoCaLize vue comme une base de données de formules du premier ordre. 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 le fragment de la logique du premier ordre des preuves ``quantitatives''. Celles-ci n'utilisent que les règles de quantification du calcul des séquents et se terminent 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 que nous affinons cependant. Nous donnons deux formalisations équivalentes de notre critère. Nous caractérisons l'admissibilité de la règle de coupure dans notre fragment par une méthode que nous pensons originale. Nous mettons en évidence une condition 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. Nous décrivons comment utiliser ces résultats dans le cadre de FoCaLiZe.