Output details
11 - Computer Science and Informatics
University of Edinburgh
Output title
An Investigation of Hilbert's Implicit Reasoning through Proof Discovery in Idle-Time
Type
E - Conference contribution
Name of conference/published proceedings
Automated Deduction in Geometry : 8th International Workshop, ADG 2010, Munich, Germany, July 22-24, 2010, Revised Selected Papers
Volume number
6877
Issue number
-
First page of article
182
ISSN of proceedings
0302-9743
Year of publication
2011
Number of additional authors
1
Additional information
<11> Originality: This is the first extensive mechanisation of Hilbert's Foundations of Geometry that aims to capture the proofs faithfully by matching their prose-like nature.
Significance: This research, aside from pushing the boundaries of formalized mathematics, provides a formal investigation by computer of a famous piece of work, which is both mathematically and historically important. It provides clear evidence that proof assistants, with the right expertise, can act as valuable tools for informed studies on mathematicians and their work.
Rigour: The reasoning is fully mechanized in the HOL Light theorem prover, thereby guaranteeing its correctness.
Interdisciplinary
-
Cross-referral requested
-
Research group
A - Centre for Intelligent Systems & their Applications
Citation count
0
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
