Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL

DOI10.1007/978-3-642-25070-5_2zbMath1350.68232OpenAlexW1457412126MaRDI QIDQ3102733

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_2

zbMATH Keywords

Euler methodnonstandard analysisdiscrete geometryIsabellemechanical theorem provingHarthong-Reeb numbers

Mathematics Subject Classification ID

Nonstandard models in mathematics (03H05) Analytic and descriptive geometry (51N99)

Related Items

Foundational aspects of multiscale digitization, Formalization of the Poincaré disc model of hyperbolic geometry, Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective

Uses Software

• Isabelle
• Isabelle/HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Insight in discrete geometry and computational content of a discrete model of the continuum
• Isabelle. A generic theorem prover
• Back and forth between continuous and discrete for the working computer scientist
• Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective
• Theorem proving in infinitesimal geometry
• Ω-Arithmetization of Ellipses
• Internal set theory: A new approach to nonstandard analysis
• A First Look into a Formal and Constructive Approach for Discrete Geometry Using Nonstandard Analysis
• Non-standard analysis