Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/6832
Tytuł: | Klein-Beltrami Model. Part II |
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 33–48 |
Abstrakt: | Tim Makarios (with Isabelle/HOL1) and John Harrison (with HOL-Light2) have shown that “the Klein-Beltrami model of the hyperbolic plane satisfy all of Tarski’s axioms except his Euclidean axiom” [2, 3, 15, 4]. With the Mizar system [1], [10] we use some ideas are taken from Tim Makarios’ MSc thesis [12] for formalized some definitions (like the tangent) and lemmas necessary for the verification of the independence of the parallel postulate. This work can be also treated as a further development of Tarski’s geometry in the formal setting [9]. |
Afiliacja: | Rue de la Brasserie 5, 7100 La Louvière, Belgium |
URI: | http://hdl.handle.net/11320/6832 |
DOI: | 10.2478/forma-2018-0004 |
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-0004.pdf | 310,35 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL