Mechanical Theorem Proving in Computational Geometry

Laura I. Meikle, Jacques Fleuriot

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

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.
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
Pages1-18
Number of pages18
ISBN (Electronic)978-3-540-31363-2
ISBN (Print)978-3-540-31332-8
DOIs
Publication statusPublished - 2006

Publication series

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

Fingerprint

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

Cite this