Show simple item record

dc.contributor.advisorFleuriot, Jacques
dc.contributor.advisorSmaill, Alan
dc.contributor.authorScott, Phil
dc.date.accessioned2016-07-12T10:31:06Z
dc.date.available2016-07-12T10:31:06Z
dc.date.issued2015-06-29
dc.identifier.urihttp://hdl.handle.net/1842/15948
dc.description.abstractThe Grundlagen der Geometrie brought Euclid’s ancient axioms up to the standards of modern logic, anticipating a completely mechanical verification of their theorems. There are five groups of axioms, each focused on a logical feature of Euclidean geometry. The first two groups give us ordered geometry, a highly limited setting where there is no talk of measure or angle. From these, we mechanically verify the Polygonal Jordan Curve Theorem, a result of much generality given the setting, and subtle enough to warrant a full verification. Along the way, we describe and implement a general-purpose algebraic language for proof search, which we use to automate arguments from the first axiom group. We then follow Hilbert through the preliminary definitions and theorems that lead up to his statement of the Polygonal Jordan Curve Theorem. These, once formalised and verified, give us a final piece of automation. Suitably armed, we can then tackle the main theorem.en
dc.contributor.sponsorEngineering and Physical Sciences Research Council (EPSRC)en
dc.language.isoenen
dc.publisherThe University of Edinburghen
dc.relation.hasversionPhil Scott and Jacques D. Fleuriot. An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time. In Automated Deduction in Geometry, Lecture Notes in Computer Science, pages 182–200. Springer, 2010.en
dc.relation.hasversionPhil Scott and Jacques D. Fleuriot. Composable Discovery Engines for Interactive Theorem Proving. In Interactive Theorem Proving, volume 6898 of Lecture Notes in Computer Science, pages 370–375. Springer, 2011.en
dc.relation.hasversionPhil Scott and Jacques D. Fleuriot. A Combinator Language for Theorem Discovery. In Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, and Volker Sorge, editors, Intelligent Computer Mathematics - 11th International Conference, volume 7362 of Lecture Notes in Computer Science, pages 371–385. Springer, 2012.en
dc.rightsAttribution-NonCommercial-ShareAlike 4.0 International*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-sa/4.0/*
dc.subjectgeometryen
dc.subjecttheorem provingen
dc.subjectproofsen
dc.titleOrdered geometry in Hilbert’s Grundlagen der Geometrieen
dc.typeThesis or Dissertationen
dc.relation.referencesDavid Hilbert. Foundations of Geometry. Open Court Classics, 2nd edition, 1971. Translated from the 10th edition of the Grundlagen der Geometrie.en
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record

Attribution-NonCommercial-ShareAlike 4.0 International
Except where otherwise noted, this item's license is described as Attribution-NonCommercial-ShareAlike 4.0 International