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