@inproceedings{77d75a3b57e14a2ea0a648feca1d477e,

title = "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.",

author = "Meikle, {Laura I.} and Jacques Fleuriot",

year = "2006",

doi = "10.1007/11615798_1",

language = "English",

isbn = "978-3-540-31332-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin Heidelberg",

pages = "1--18",

booktitle = "Automated Deduction in Geometry",

}