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

DOI10.1007/978-3-642-25070-5_11zbMath1350.68244OpenAlexW1708936760MaRDI QIDQ3102743

Phil Scott, Jacques D. Fleuriot

Publication date: 25 November 2011

Published in: Automated Deduction in Geometry (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-25070-5_11

Mathematics Subject Classification ID

Metric geometry (51F99)

Related Items

From informal to formal proofs in Euclidean geometry ⋮ Formalization of the Poincaré disc model of hyperbolic geometry ⋮ Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL

Uses Software

• HOL Light
• Flyspeck

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A case study in formalizing projective geometry in Coq: Desargues theorem
• Hilbert's ``Grundlagen der Geometrie
• Edinburgh LCF. A mechanized logic of computation
• Composable Discovery Engines for Interactive Theorem Proving
• Formalizing Hilbert’s Grundlagen in Isabelle/Isar
• The use of machines to assist in rigorous proof
• Automated Deduction in Geometry
• David Hilbert and his mathematical work