Formal study of plane Delaunay triangulation

Résumé : Cet article présente la preuve formelle de correction d'un algorithme de triangulation de Delaunay. L'algorithme consiste à répéter une opération de basculement d'arête à partir d'une triangulation initial jusqu'à ce que la propriété de Delaunay soit satisfaite. Pour décrire les triangulations, nous utilisons un cadre formel d'hypercartes combinatoires que nous développons depuis des années. Nous plongeons les hypercartes dans le plan en attachant des coordonnées aux élément de l'hypercarte de façon cohérente. Nous décrivons ensuite quelles sont les arêtes illégales pour Delaunay et comment fonctionne l'opération de basculement, pour laquelle nous montrons la préservations des structures d'hypercarte, de triangultion, et de plongement. Pour prouver la terminaison de l'algorithme, nous utilisons une approche générique exprimant que toute relation non-cyclic sur un ensemble fini est bien fondée.
Type de document :
Communication dans un congrès
Paulson, Lawrence and Kaufmann, Matt. Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. Springer, 6172, pp.211-226, 2010, Lecture Notes in Computer Science; Interactive Theorem Proving. <http://www.springerlink.com/content/yk74674271411315/fulltext.pdf>
Liste complète des métadonnées


https://hal.inria.fr/inria-00504027
Contributeur : Yves Bertot <>
Soumis le : lundi 19 juillet 2010 - 16:09:27
Dernière modification le : lundi 5 octobre 2015 - 17:00:46
Document(s) archivé(s) le : vendredi 22 octobre 2010 - 15:53:32

Fichiers

Del-ITP10.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00504027, version 1
  • ARXIV : 1007.3350

Collections

Citation

Jean-François Dufourd, Yves Bertot. Formal study of plane Delaunay triangulation. Paulson, Lawrence and Kaufmann, Matt. Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. Springer, 6172, pp.211-226, 2010, Lecture Notes in Computer Science; Interactive Theorem Proving. <http://www.springerlink.com/content/yk74674271411315/fulltext.pdf>. <inria-00504027>

Partager

Métriques

Consultations de
la notice

274

Téléchargements du document

207