Mechanical theorem proving in computational geometry

Abstract

Algorithms for solving geometric problems are widely used in many scientific disciplines. Applications range from computer vision and robotics to molecular biology and astrophysics. Proving the correctness of these algorithms is vital in order to boost confidence in them. By specifying the algorithms formally in a theorem prover such as Isabelle, it is hoped that rigorous proofs showing their correctness will be obtained. This paper outlines our current framework for reasoning about geometric algorithms in Isabelle. It focuses on our case study of the convex hull problem and shows how Hoare logic can be used to prove the correctness of such algorithms. © Springer-Verlag Berlin Heidelberg 2006.