In this paper, we describe how we captured and investigated incidence reasoning in Hilbert’s Foundations of Geometry by using a new discovery tool integrated into an interactive proof assistant. Our tool exploits concurrency, inferring facts independently of the user with the incomplete proof as a guide. It explores the proof space, contributes tedious lemmas and discovers alternative proofs. We show how this tool allowed us to write readable formalised proof-scripts that correspond very closely to Hilbert’s prose arguments.
|Title of host publication||Automated Deduction in Geometry|
|Subtitle of host publication||8th International Workshop, ADG 2010, Munich, Germany, July 22-24, 2010, Revised Selected Papers|
|Editors||Pascal Schreck, Julien Narboux, Jürgen Richter-Gebert|
|Number of pages||19|
|Publication status||Published - 2011|
|Name||Lecture Notes in Computer Science|
|Publisher||Springer Berlin / Heidelberg|