Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq

Autor: Charly Gries, Pascal Schreck, Pierre Boutry, Julien Narboux

Publikováno v: Journal of Automated Reasoning
Journal of Automated Reasoning, Springer Verlag, 2019, 62 (1), pp.68. ⟨10.1007/s10817-017-9422-8⟩
Journal of Automated Reasoning, 2019, 62 (1), pp.68. ⟨10.1007/s10817-017-9422-8⟩

online first; International audience; In this paper we focus on the formalization of the proofs of equivalence between different versions of Euclid's 5 th postulate. Our study is performed in the context of Tarski's neutral geometry, or equivalently

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5295cfedebbea0e5f43a1d51340f29ca
https://hal.inria.fr/hal-01178236v2/document