14-18 juin 2021 Virtuelle (France)
Un prouveur automatique pour la géométrie projective et son intégration à Coq
Nicolas Magaud  1@  
1 : Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie  (ICube)  -  Site web
Centre National de la Recherche Scientifique : UMR7357, université de Strasbourg : FR3627
300 bd Sébastien Brant - BP 10413 - F-67412 Illkirch Cedex -  France

Afin de pouvoir démontrer formellement la correction d'algorithmes géométriques en Coq, il est nécessaire de disposer d'outils pour automatiser au moins partiellement les démonstrations en géométrie. Nous étudions cette question dans le cadre simple de la géométrie projective en utilisant une approche combinatoire et la notion de rang d'un ensemble de points. L'outil proposé, implanté en C, procède par saturation du contexte et permet de démontrer automatiquement de nombreux théorèmes emblématiques de la géométrie projective. Afin de s'assurer de la correction de ces démonstrations, l'outil produit une trace sous la forme d'un script de preuve, qui est ensuite vérifié par Coq.


Personnes connectées : 35 Vie privée
Chargement...