Formalizing convex hull algorithms

DOI10.1007/3-540-44755-5_24MaRDI QIDQ4790670zbMATH OpenFDO

Authors David Pichardie, Yves Bertot

Publication date 4 February 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2152/21520346

Mathematics Subject Classification ID

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

Recommendations

• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• Formal proof in Coq and derivation of an imperative program to compute convex hulls
• Automated Deduction in Geometry
• The quickhull algorithm for convex hulls

Cited in

(16)

• Formal verification of a geometry algorithm: a quest for abstract views and symmetry in Coq proofs
• A verified ODE solver and the Lorenz attractor
• Formalizing generalized maps in Coq
• Formalization of the Poincaré disc model of hyperbolic geometry
• Design and formal proof of a new optimal image segmentation program with hypermaps
• Formal proof in Coq and derivation of an imperative program to compute convex hulls
• Formal specification and proofs for the topology and classification of combinatorial surfaces
• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• Verification of Closest Pair of Points Algorithms
• Mechanical Theorem Proving in Tarski’s Geometry
• Automated Deduction in Geometry
• Numerical statistical modeling of optical radiation transfer in random crystal media
• Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
• Safe smooth paths between straight line obstacles
• Formally verifying a vertical cell decomposition algorithm
• Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof

This page was built for publication: Formalizing convex hull algorithms

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