Please use this identifier to cite or link to this item:
https://research.matf.bg.ac.rs/handle/123456789/601| Title: | Formalization of the Poincaré Disc Model of Hyperbolic Geometry | Authors: | Simić, Danijela Marić, Filip Boutry, Pierre |
Affiliations: | Informatics and Computer Science Informatics and Computer Science |
Keywords: | Formalization of geometry;Isabelle/HOL;Poincaré model | Issue Date: | 1-Jan-2021 | Journal: | Journal of Automated Reasoning | 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 CP1and 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. |
URI: | https://research.matf.bg.ac.rs/handle/123456789/601 | ISSN: | 01687433 | DOI: | 10.1007/s10817-020-09551-2 |
| Appears in Collections: | Research outputs |
Show full item record
SCOPUSTM
Citations
3
checked on Dec 22, 2024
Page view(s)
14
checked on Dec 24, 2024
Google ScholarTM
Check
Altmetric
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.