Name
Abstract | ||
|---|---|---|
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. |
Year | Venue | Keywords |
|---|---|---|
2001 | TPHOLs | computational geometry,formalizing convex hull algorithms,special attention,conventional algorithm presentation,convex hull computation,basic principle,formal description,mathematical proof,convex hull algorithms work,convex hull |
Field | DocType | ISBN |
Convex hull algorithms,Computer science,Automated theorem proving,Computational geometry,Algorithm,Convex polygon,Convex hull,Theoretical computer science,Mathematical proof,Formal verification,Computation | Conference | 3-540-42525-X |
Citations | PageRank | References |
22 | 1.25 | 3 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| david pichardie | 1 | 488 | 33.73 |
| Yves Bertot | 2 | 442 | 40.82 |