Mechanising Hilbert's Foundations of Geometry in Isabelle
Phil Scott · 2008
This project continues and revises Meikle’s mechanisation of Hilbert’s Foundations of Geometry in Isabelle/HOL, focusing on declarative-style proofs to create readable and maintainable proof documents. In the interests of readability and conciseness, we have investigated general-purpose abstractions for geometric reasoning, and have shown how these can simplify existing proofs. We have revised many of the existing definitions by introducing new types, and analysed the notion of rays and half-planes more deeply than Hilbert had originally. Finally, we have corrected subtle mistakes in Meikle’s mechanised axioms of Group III, forcing us to produce new corrected proofs of the early theorems. i Acknowledgements I cannot give enough thanks to my supervisors, Jacques Fleuriot and Laura Meikle. I would be fortunate enough to have even one supervisor with their knowledge, dedication and passion for the subject matter. ii Declaration I declare that this thesis was composed by myself, that the work contained herein is