Identifiant pérenne de la notice : 226513645
Notice de type
Notice de regroupement
Note publique d'information : Le logiciel Coq est un assistant à la preuve basé sur le Calcul des Constructions
Inductives. Dans cette thèse, nous proposons d’améliorer l’automatisation de ce système
en le dotant d’une procédure de décision réflexive et complète pour la théorie du
premier ordre de l’arithmétique réelle. La théorie des types implémentée par le système
Coq comprend un langage fonctionnel typé dans lequel nous avons programmé un algorithme
de Décomposition Algébrique Cylindrique (CAD). Cet algorithme calcule une partition
de l’espace en cellules semi-algébriques sur lesquelles tous les polynômes d’une famille
donnée ont un signe constant et permet ainsi de décider les formules de cette théorie.
Il s’agit ensuite de prouver la correction de l’algorithme et de la procédure de décision
associée avec l’assistant de la preuve Coq. Ce travail comprend en particulier une
librairie d’arithmétique polynomiale certifiée et une partie significative de la preuve
formelle de correction de l’algorithme des sous-résultants. Ce dernier algorithme
permet de calculer efficacement le plus grand commun diviseur de polynômes à coefficients
dans un anneau, en particulier à plusieurs variables. Nous proposons également une
tactique réflexive de décision des égalités dans les structures d’anneaux et de semi-anneaux
qui améliore les performances de l’outil déjà disponible et augmente son spectre d’action
en exploitant les possibilités de calcul du système. Dans une dernière partie, nous
étudions le contenu calculatoire d’une preuve constructive d’un lemme élémentaire
d’analyse réelle, le principe d’induction ouverte.
Note publique d'information : The Coq system is a proof assistant based on the Calculus of Inductive Constructions.
In this work, we propose to enhance the automation of this system by providing a reflexive
and complete decision procedure for the first order theory of real numbers. The Type
Theory implemented by the Coq system comprises a typed functional programming language,
which we have used to implement a Cylindrical Algebraic Decomposition algorithm (CAD).
This algorithm computes a partition of the space into sign-invariant, semi-algebraic
cells for the polynomials of a given family. Hence it allows deciding all the formulae
of this theory. Then we have to prove formally the corrections of the algorithm and
of the related decision procedure, using the Coq proof assistant. This work includes
a library for certified polynomial arithmetic and a significant part of the format
proof of correctness of the sub-resultants algorithm. This last algorithm allows computing
efficiently the greatest common divisor of polynomials with coefficients in a ring,
and in particular of multivariate polynomials. We also propose a reflexive tactic
for deciding equalities in ring and semi-ring structures, which enhances the performances
of the tool previously available in the system by taking benefit of the computational
abilities of the system. In a last part, we study the computational content of a constructive
proof of an elementary lemma of real analysis, called principle of open induction.
paprika.idref.fr
data.idref.fr
Documentation
