Theorem of three circles in Coq

Julianna Zsidó 1, *
* Auteur correspondant
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Résumé : Le théorème de trois cercles en géométrie algébrique réelle garantit la terminaison et la correction d'un algorithme d'isolation de racines réelles d'un polynôme univarié. L'idée générale de la preuve est de considérer des polynômes dont les racines appartiennent à des secteurs du plan complexe bornés par des droites. Après avoir appliqué une transformation du plan contenant une inversion, ces secteurs sont transformés en secteurs bornés par des cercles. Nous formalisons cette preuve plutôt géométrique en Ssreflect, qui est une extension de l'assistante de preuve Coq, mettant des outils algébriques puissants à notre disposition. Ils nous permettent de formaliser la preuve d'un point de vue algébrique.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2013, 〈10.1007/s10817-013-9299-0〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00864827
Contributeur : Julianna Zsido <>
Soumis le : lundi 23 septembre 2013 - 12:58:39
Dernière modification le : jeudi 11 janvier 2018 - 15:51:00

Lien texte intégral

Identifiants

Collections

Citation

Julianna Zsidó. Theorem of three circles in Coq. Journal of Automated Reasoning, Springer Verlag, 2013, 〈10.1007/s10817-013-9299-0〉. 〈hal-00864827〉

Partager

Métriques

Consultations de la notice

189