Formalization of the Poincaré Disc Model of Hyperbolic Geometry - Archive ouverte HAL Access content directly
Journal Articles Journal of Automated Reasoning Year : 2020

Formalization of the Poincaré Disc Model of Hyperbolic Geometry

(1) , (1) , (2, 3)
1
2
3

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.
Fichier principal
Vignette du fichier
Poincare.pdf (533.14 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03120829 , version 1 (25-01-2021)

Identifiers

Cite

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

Altmetric

Share

Gmail Facebook Twitter LinkedIn More