Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/6831
Tytuł: | Klein-Beltrami Model. Part I |
Autorzy: | Coghetto, Roland |
Słowa kluczowe: | Tarski’s geometry axioms foundations of geometry Klein-Beltrami model |
Data wydania: | 2018 |
Data dodania: | 20-sie-2018 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 26, Issue 1, Pages 21–32 |
Abstrakt: | Tim Makarios (with Isabelle/HOL1) and John Harrison (with HOL-Light2) shown that “the Klein-Beltrami model of the hyperbolic plane satisfy all of Tarski’s axioms except his Euclidean axiom” [3], [4], [14], [5]. With the Mizar system [2], [7] we use some ideas are taken from Tim Makarios’ MSc thesis [13] for the formalization of some definitions (like the absolute) and lemmas necessary for the verification of the independence of the parallel postulate. This work can be also treated as further development of Tarski’s geometry in the formal setting [6]. Note that the model presented here, may also be called “Beltrami-Klein Model”, “Klein disk model”, and the “Cayley-Klein model” [1]. |
Afiliacja: | Rue de la Brasserie 5, 7100 La Louvière, Belgium |
URI: | http://hdl.handle.net/11320/6831 |
DOI: | 10.2478/forma-2018-0003 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
Typ Dokumentu: | Article |
Występuje w kolekcji(ach): | Formalized Mathematics, 2018, Volume 26, Issue 1 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma-2018-0003.pdf | 300,74 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL