On Constructive-Deductive Method For Plane Euclidean Geometry
Evgeny V. Ivashkevich
TL;DR
This paper formalizes a constructive-deductive approach to plane Euclidean geometry within Coq, combining postulates for geometric constructions and axioms for properties of figures, offering a constructive alternative to Hilbert's system.
Contribution
It introduces a formalized constructive-deductive system for Euclidean geometry in Coq, integrating elementary constructions and properties as a novel framework.
Findings
Successfully formalized the system in Coq
Provides a constructive version of Hilbert's axiomatization
Enables formal proof development in Euclidean geometry
Abstract
Constructive-deductive method for plane Euclidean geometry is proposed and formalized within Coq Proof Assistant. This method includes both postulates that describe elementary constructions by idealized geometric tools (pencil, straightedge and compass), and axioms that describes properties of basic geometric figures (points, lines, circles and triangles). The proposed system of postulates and axioms can be considered as a constructive version of the Hilbert's formalization of plane Euclidean geometry.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Theoretical and Applied Studies in Material Sciences and Geometry · Mathematics and Applications · History and Theory of Mathematics