On Constructive-Deductive Method For Plane Euclidean Geometry
From MaRDI portal
Publication:6315493
arXiv1903.05175MaRDI QIDQ6315493
Author name not available (Why is that?)
Publication date: 12 March 2019
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.
Has companion code repository: https://github.com/ivashkev/math-formalizations
This page was built for publication: On Constructive-Deductive Method For Plane Euclidean Geometry
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6315493)
