Skip to Main content Skip to Navigation
Journal articles

Formalization of the Poincaré Disc Model of Hyperbolic Geometry

Abstract : We describe formalization of the Poincaré disc model of hyperbolic geometry within the Isabelle/HOL proof assistant. The model is defined within the complex projective line ℂP1 and is shown to satisfy Tarski's axioms except for Euclid's axiom — it is shown to satisfy it's negation, and, moreover, to satisfy the existence of limiting parallels axiom.
Document type :
Journal articles
Complete list of metadata
Contributor : Pierre Boutry Connect in order to contact the contributor
Submitted on : Monday, January 25, 2021 - 10:16:12 PM
Last modification on : Thursday, December 2, 2021 - 3:17:04 AM
Long-term archiving on: : Monday, April 26, 2021 - 7:33:13 PM


Files produced by the author(s)



Danijela Simić, Filip Marić, Pierre Boutry. Formalization of the Poincaré Disc Model of Hyperbolic Geometry. Journal of Automated Reasoning, Springer Verlag, 2020, 65 (1), pp.31-73. ⟨10.1007/s10817-020-09551-2⟩. ⟨hal-03120829⟩



Les métriques sont temporairement indisponibles