Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/9220
Tytuł: | Klein-Beltrami model. Part IV |
Autorzy: | Coghetto, Roland |
Słowa kluczowe: | Tarski’s geometry axioms foundations of geometry Klein-Beltrami model |
Data wydania: | 2020 |
Data dodania: | 10-cze-2020 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 28, Issue 1, Pages 9-21 |
Abstrakt: | Timothy 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” [2],[3],[4, 5]. With the Mizar system [1] we use some ideas taken from Tim Makarios’s MSc thesis [10] to formalize some definitions and lemmas necessary for the verification of the independence of the parallel postulate. In this article, which is the continuation of [8], we prove that our constructed model satisfies the axioms of segment construction, the axiom of betweenness identity, and the axiom of Pasch due to Tarski, as formalized in [11] and related Mizar articles. |
Afiliacja: | Rue de la Brasserie 5, 7100 La Louvière, Belgium |
URI: | http://hdl.handle.net/11320/9220 |
DOI: | 10.2478/forma-2020-0002 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
metadata.dc.identifier.orcid: | 0000-0002-4901-0766 |
Typ Dokumentu: | Article |
metadata.dc.rights.uri: | http://creativecommons.org/licenses/by-sa/3.0/pl/ |
Występuje w kolekcji(ach): | Formalized Mathematics, 2020, Volume 28, Issue 1 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma_2020_28_01_0002.pdf | 293,51 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL