Automation for Geometry in Isabelle/HOL
Laura I. Meikle, Jacques Fleuriot · EPiC series in computing · 2018
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.