publication . Preprint . 2019

# On Constructive-Deductive Method For Plane Euclidean Geometry

Ivashkevich, Evgeny V.;
Open Access English
• Published: 12 Mar 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.
Subjects
free text keywords: Mathematics - Logic, Mathematics - Metric Geometry

[12] Gilles Kahn. Constructive geometry. (Coq Proof Assistant). https://github.com/coq-contribs/constructive-geometry, 2008.

[13] Michael Beeson, Pierre Boutry, Gabriel Braun, Charly Gries, Julien Narboux, and Dan Song. GeoCoq. (Coq Proof Assistant). https://github.com/GeoCoq/GeoCoq, 2015.

[14] A.V. Pogorelov. Elementary Geometry (in Russian). Nauka Moscow, 1974.

[15] Jeremy Avigad, Edward Dean, and John Mumma. A formal system for Euclid's elements. Review of Symbolic Logic, 2(4):700-768, 2009.

[16] Ariel Kellison, Mark Bickford, and Robert Constable. Implementing Euclid's straightedge and compass constructions in type theory. Annals of Mathematics and Artificial Intelligence, 85(2):175-192, 2019.

• software
• software
• software
##### GeoCoq software on GitHub in support of 'On Constructive-Deductive Method For Plane 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.
Subjects
free text keywords: Mathematics - Logic, Mathematics - Metric Geometry

[12] Gilles Kahn. Constructive geometry. (Coq Proof Assistant). https://github.com/coq-contribs/constructive-geometry, 2008.

[13] Michael Beeson, Pierre Boutry, Gabriel Braun, Charly Gries, Julien Narboux, and Dan Song. GeoCoq. (Coq Proof Assistant). https://github.com/GeoCoq/GeoCoq, 2015.

[14] A.V. Pogorelov. Elementary Geometry (in Russian). Nauka Moscow, 1974.

[15] Jeremy Avigad, Edward Dean, and John Mumma. A formal system for Euclid's elements. Review of Symbolic Logic, 2(4):700-768, 2009.

[16] Ariel Kellison, Mark Bickford, and Robert Constable. Implementing Euclid's straightedge and compass constructions in type theory. Annals of Mathematics and Artificial Intelligence, 85(2):175-192, 2019.

• software
• software
• software