Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/9219
Tytuł: | Klein-Beltrami model. Part III |
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 1-7 |
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 (like the absolute) and lemmas necessary for the verification of the independence of the parallel postulate. In this article we prove that our constructed model (we prefer “Beltrami-Klein” name over “Klein-Beltrami”, which can be seen in the naming convention for Mizar functors, and even MML identifiers) satisfies the congruence symmetry, the congruence equivalence relation, and the congruence identity axioms formulated by Tarski (and formalized in Mizar as described briefly in [8]). |
Afiliacja: | Rue de la Brasserie 5, 7100 La Louvière, Belgium |
URI: | http://hdl.handle.net/11320/9219 |
DOI: | 10.2478/forma-2020-0001 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
metadata.dc.identifier.orcid: | 0000-0002-4901-0766 |
Typ Dokumentu: | Article |
metadata.dc.rights.uri: | https://creativecommons.org/licenses/by-sa/3.0/ |
Występuje w kolekcji(ach): | Formalized Mathematics, 2020, Volume 28, Issue 1 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma_2020_28_01_0001.pdf | 266,3 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL