On Constructive-Deductive Method For Plane Euclidean Geometry
E. Ivashkevich. (2019)cite arxiv:1903.05175Comment: 45 pages,16 figures, 6 tables.
Zusammenfassung
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.
Beschreibung
[1903.05175] On Constructive-Deductive Method For Plane Euclidean Geometry
%0 Journal Article
%1 ivashkevich2019constructivedeductive
%A Ivashkevich, Evgeny V.
%D 2019
%K geometry mathematics readings
%T On Constructive-Deductive Method For Plane Euclidean Geometry
%U http://arxiv.org/abs/1903.05175
%X 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.
@article{ivashkevich2019constructivedeductive,
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.},
added-at = {2020-01-20T14:14:31.000+0100},
author = {Ivashkevich, Evgeny V.},
biburl = {https://www.bibsonomy.org/bibtex/21c4781c5e9c4f42098774849e653b5ed/kirk86},
description = {[1903.05175] On Constructive-Deductive Method For Plane Euclidean Geometry},
interhash = {c934853d587f25a19729ca91fb8d4a9e},
intrahash = {1c4781c5e9c4f42098774849e653b5ed},
keywords = {geometry mathematics readings},
note = {cite arxiv:1903.05175Comment: 45 pages,16 figures, 6 tables},
timestamp = {2020-01-20T14:15:00.000+0100},
title = {On Constructive-Deductive Method For Plane Euclidean Geometry},
url = {http://arxiv.org/abs/1903.05175},
year = 2019
}