Automated Generation of Illustrations for Synthetic Geometry Proofs

Autor: Predrag Janičić, Julien Narboux

Publikováno v: Proceedings of Automated Deduction in Geometry 2021
Automated Deduction in Geometry
Automated Deduction in Geometry, Zoltán Kovács, Sep 2021, Hagenberg, Austria

We report on a new, simple, modular, and flexible approach for automated generation of illustrations for (readable) synthetic geometry proofs. The underlying proofs are generated using the Larus automated prover for coherent logic, and corresponding

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::63d2e376e8dfb1d079b1b277fa948585
https://doi.org/10.4204/eptcs.352.9

Proof-checking Euclid

Autor: Freek Wiedijk, Michael Beeson, Julien Narboux

Publikováno v: Annals of Mathematics and Artificial Intelligence
Annals of Mathematics and Artificial Intelligence, 2019, pp.53. ⟨10.1007/s10472-018-9606-x⟩
Annals of Mathematics and Artificial Intelligence, 85, 2-4, pp. 213-257
Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2019, pp.53. ⟨10.1007/s10472-018-9606-x⟩
Annals of Mathematics and Artificial Intelligence, 85, 213-257

We used computer proof-checking methods to verify the correctness of our proofs of the propositions in Euclid Book I. We used axioms as close as possible to those of Euclid, in a language closely related to that used in Tarski's formal geometry. We u

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::aea93a5c512a30eb3feab607e2897a27
https://hdl.handle.net/2066/201509

Formalization of the Arithmetization of Euclidean Plane Geometry and Applications

Autor: Pierre Boutry, Julien Narboux, Gabriel Braun

Publikováno v: Journal of Symbolic Computation
Journal of Symbolic Computation, Elsevier, 2019, Special Issue on Symbolic Computation in Software Science, 90, pp.149-168. ⟨10.1016/j.jsc.2018.04.007⟩
James H. Davenport and Temur Kutsia
Journal of Symbolic Computation, 2019, Special Issue on Symbolic Computation in Software Science, 90, pp.149-168. ⟨10.1016/j.jsc.2018.04.007⟩

International audience; This paper describes the formalization of the arithmetization of Euclidean plane geometry in the Coq proof assistant. As a basis for this work, Tarski's system of geometry was chosen for its well-known metamath-ematical proper

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d19606004baeac5b5c1824c21361cd57
https://hal.inria.fr/hal-01483457/file/extended-arithmetization.pdf

A Synthetic Proof of Pappus’ Theorem in Tarski’s Geometry

Autor: Gabriel Braun, Julien Narboux

Publikováno v: Journal of Automated Reasoning
Journal of Automated Reasoning, Springer Verlag, 2017, 58 (2), pp.23. ⟨10.1007/s10817-016-9374-4⟩
Journal of Automated Reasoning, 2017, 58 (2), pp.23. ⟨10.1007/s10817-016-9374-4⟩

International audience; In this paper, we report on the formalization of a synthetic proof of Pappus' theorem. We provide two versions of the theorem: the first one is proved in neutral geometry (without assuming the parallel postulate), the second (

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7977d8284fd5f632849f3a8fc40dcce3
https://doi.org/10.1007/s10817-016-9374-4

Towards A Certified Version of the Encyclopedia of Triangle Centers

Autor: Julien Narboux, David Braun

Publikováno v: Mathematics in Computer Science
Mathematics in Computer Science, 2016, 10 (1), pp.17. ⟨10.1007/s11786-016-0254-4⟩
Mathematics in Computer Science, Springer, 2016, 10 (1), pp.17. ⟨10.1007/s11786-016-0254-4⟩

International audience; Triangle centers such as the center of gravity, the circumcenter, the orthocenter are well studied by geometers. Recently, under the guidance of Clark Kimberling, an electronic encyclopedia of triangle centers (ETC) has been d

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::021a26c98370b0df3cc72a8f8dfe4455
https://inria.hal.science/hal-01174131v2/file/certified-etc.pdf