Automation for Geometry in Isabelle/HOL

Laura Meikle, Jacques Fleuriot

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

Abstract / Description of output

In this paper we describe a number of automation techniques which we have developed to assist us in reasoning formally about geometry in the interactive theorem prover Isabelle. These range from simplification rules to a user-centric integration of Isabelle with the computer algebra system QEPCAD-B. We demonstrate the power and limitations of these techniques through illustrative examples taken from our verification of a triangulation algorithm.
Original languageEnglish
Title of host publicationPAAR-2010: Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning
EditorsRenate A. Schmidt, Stephan Schulz, Boris Konev
PublisherEasyChair
Pages84-94
Number of pages11
Publication statusPublished - 2012

Publication series

NameEasyChair Proceedings in Computing
PublisherEasyChair
Volume9
ISSN (Electronic)2040-557X

Fingerprint

Dive into the research topics of 'Automation for Geometry in Isabelle/HOL'. Together they form a unique fingerprint.

Cite this