Formal study of plane Delaunay triangulation

DOI10.1007/978-3-642-14052-5_16MaRDI QIDQ5747651zbMATH OpenOpenAlexFDO

Authors Jean-François Dufourd, Yves Bertot

Publication date 14 September 2010

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1007.3350

Mathematics Subject Classification ID

Computer graphics; computational geometry (digital and algorithmic aspects) (68U05)

Abstract: This article presents the formal proof of correctness for a plane Delaunay triangulation algorithm. It consists in repeating a sequence of edge flippings from an initial triangulation until the Delaunay property is achieved. To describe triangulations, we rely on a combinatorial hypermap specification framework we have been developing for years. We embed hypermaps in the plane by attaching coordinates to elements in a consistent way. We then describe what are legal and illegal Delaunay edges and a flipping operation which we show preserves hypermap, triangulation, and embedding invariants. To prove the termination of the algorithm, we use a generic approach expressing that any non-cyclic relation is well-founded when working on a finite set.

Recommendations

• NUMERICAL STABILITY OF ALGORITHMS FOR 2D DELAUNAY TRIANGULATIONS
• An optimal algorithm for realizing a Delaunay triangulation
• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• Generalized Delaunay triangulation for planar graphs
• scientific article; zbMATH DE number 6379407

Cited in

(10)

• Formal verification of a geometry algorithm: a quest for abstract views and symmetry in Coq proofs
• Formalization of the Poincaré disc model of hyperbolic geometry
• Graph theory in Coq: minors, treewidth, and isomorphisms
• Formal specification and proofs for the topology and classification of combinatorial surfaces
• Characterizing Delaunay graphs via fixed point theorem: a simple proof
• Formal study of functional orbits in finite domains
• Verification of Closest Pair of Points Algorithms
• Formalizing Pick's theorem in Isabelle/HOL
• Safe smooth paths between straight line obstacles
• A computer-assisted proof of correctness of a marching cubes algorithm

Describes a project that uses

Uses Software

• MPFR
• 2D triangulations

This page was built for publication: Formal study of plane Delaunay triangulation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5747651)