Formal study of plane Delaunay triangulation

Details Formal study of plane Delaunay triangulation Formal study of plane Delaunay triangulation

2010-07-20

arxiv.org/abs/1007.3350v1

Interactive Theorem Priving, Edinburgh : United Kingdom (2010)

Computer Science

Logic in Computer Science

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Formal study of plane Delaunay triangulation does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Formal study of plane Delaunay triangulation, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Formal study of plane Delaunay triangulation will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-125139