An Investigation of Hilbert's Implicit Reasoning through Proof Discovery in Idle-Time

Phil Scott, Jacques Fleuriot

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

Abstract

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.
Original languageEnglish
Title of host publicationAutomated Deduction in Geometry
Subtitle of host publication8th International Workshop, ADG 2010, Munich, Germany, July 22-24, 2010, Revised Selected Papers
EditorsPascal Schreck, Julien Narboux, Jürgen Richter-Gebert
PublisherSpringer-Verlag GmbH
Pages182-200
Number of pages19
ISBN (Electronic)978-3-642-25070-5
ISBN (Print)978-3-642-25069-9
DOIs
Publication statusPublished - 2011

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
Volume6877
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'An Investigation of Hilbert's Implicit Reasoning through Proof Discovery in Idle-Time'. Together they form a unique fingerprint.

Cite this