Mechanical Theorem Proving in Computational Geometry

Laura I. Meikle, Jacques Fleuriot

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationAutomated Deduction in Geometry
Subtitle of host publication5th International Workshop, ADG 2004, Gainesville, FL, USA, September 16-18, 2004. Revised Papers
Place of PublicationBerlin, Heidelberg
PublisherSpringer Berlin Heidelberg
Number of pages18
ISBN (Electronic)978-3-540-31363-2
ISBN (Print)978-3-540-31332-8
Publication statusPublished - 2006

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


Dive into the research topics of 'Mechanical Theorem Proving in Computational Geometry'. Together they form a unique fingerprint.

Cite this