We study the development of formally proved algorithms for computational geometry. The result of this work is a formal description of the basic principles that make convex hull algorithms work and two programs that implement convex hull computation and have been automatically obtained from formally verified mathematical proofs. A special attention has been given to handling degenerate cases that are often overlooked by conventional algorithm presentations.
CITATION STYLE
Pichardie, D., & Bertot, Y. (2001). Formalizing convex hull algorithms. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2152, pp. 346–361). Springer Verlag. https://doi.org/10.1007/3-540-44755-5_24
Mendeley helps you to discover research relevant for your work.