REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

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: 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 RozmiarFormat 
forma_2020_28_01_0001.pdf266,3 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki


Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons