REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

  1. Repozytorium Uniwersytetu w Białymstoku
  2. Czasopisma naukowe / Journals
  3. Formalized Mathematics
  4. Formalized Mathematics, 2018, Volume 26, Issue 1

Szukanie zaawansowane
  • Zespoły i Kolekcje


  • Zaloguj się
  • Zarejestruj się
  • Mój RUB
  • FAQ
  • Polityka
  • Regulamin
  • DOI
  • Instrukcja
  • Aspekty prawne
  • Open Access
  • Archiwum


  • Kontakt
  • O Dspace
  • Strona Biblioteki
  • Strona Uczelni



    • Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/6831
    Pełny rekord metadanych
    Pole DCWartośćJęzyk
    dc.contributor.authorCoghetto, Roland-
    dc.date.accessioned2018-08-20T06:41:51Z-
    dc.date.available2018-08-20T06:41:51Z-
    dc.date.issued2018-
    dc.identifier.citationFormalized Mathematics, Volume 26, Issue 1, Pages 21–32-
    dc.identifier.issn1426-2630-
    dc.identifier.urihttp://hdl.handle.net/11320/6831-
    dc.description.abstractTim 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].-
    dc.language.isoen-
    dc.publisherDeGruyter Open-
    dc.subjectTarski’s geometry axioms-
    dc.subjectfoundations of geometry-
    dc.subjectKlein-Beltrami model-
    dc.titleKlein-Beltrami Model. Part I-
    dc.typeArticle-
    dc.identifier.doi10.2478/forma-2018-0003-
    dc.description.AffiliationRue de la Brasserie 5, 7100 La Louvière, Belgium-
    dc.description.referencesNorbert A’Campo and Athanase Papadopoulos. On Klein’s so-called non-Euclidean geometry. arXiv preprint arXiv:1406.7309, 2014.-
    dc.description.referencesGrzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.-
    dc.description.referencesEugenio Beltrami. Saggio di interpetrazione della geometria non-euclidea. Giornale di Matematiche, 6:284–322, 1868.-
    dc.description.referencesEugenio Beltrami. Essai d’interprétation de la géométrie non-euclidéenne. In Annales scientifiques de l’École Normale Supérieure. Trad. par J. Hoüel, volume 6, pages 251–288. Elsevier, 1869.-
    dc.description.referencesKarol Borsuk and Wanda Szmielew. Podstawy geometrii. Państwowe Wydawnictwo Naukowe, Warszawa, 1955 (in Polish).-
    dc.description.referencesAdam Grabowski. Tarski’s geometry modelled in Mizar computerized proof assistant. In Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, FedCSIS 2016, Gdańsk, Poland, September 11–14, 2016, pages 373–381, 2016. doi:10.15439/2016F290.-
    dc.description.referencesAdam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.-
    dc.description.referencesKanchun, Hiroshi Yamazaki, and Yatsuka Nakamura. Cross products and tripple vector products in 3-dimensional Euclidean space. Formalized Mathematics, 11(4):381–383, 2003.-
    dc.description.referencesArtur Korniłowicz and Yasunari Shidama. Intersections of intervals and balls in 𝒠Tn . Formalized Mathematics, 12(3):301–306, 2004.-
    dc.description.referencesArtur Korniłowicz and Yasunari Shidama. Some properties of circles on the plane. Formalized Mathematics, 13(1):117–124, 2005.-
    dc.description.referencesAkihiro Kubo. Lines in n -dimensional Euclidean spaces. Formalized Mathematics, 11(4): 371–376, 2003.-
    dc.description.referencesXiquan Liang, Piqing Zhao, and Ou Bai. Vector functions and their differentiation formulas in 3-dimensional Euclidean spaces. Formalized Mathematics, 18(1):1–10, 2010. doi:10.2478/v10037-010-0001-2.-
    dc.description.referencesTimothy James McKenzie Makarios. A mechanical verification of the independence of Tarski’s Euclidean Axiom. Victoria University of Wellington, New Zealand, 2012. Master’s thesis.-
    dc.description.referencesAndrzej Trybulec. A Borsuk theorem on homotopy types. Formalized Mathematics, 2(4): 535–545, 1991.-
    dc.description.referencesXiaopeng Yue, Xiquan Liang, and Zhongpin Sun. Some properties of some special matrices. Formalized Mathematics, 13(4):541–547, 2005.-
    dc.identifier.eissn1898-9934-
    dc.description.volume26-
    dc.description.issue1-
    dc.description.firstpage21-
    dc.description.lastpage32-
    dc.identifier.citation2Formalized Mathematics-
    Występuje w kolekcji(ach):Formalized Mathematics, 2018, Volume 26, Issue 1

    Pliki w tej pozycji:
    Plik Opis RozmiarFormat 
    forma-2018-0003.pdf300,74 kBAdobe PDFOtwórz
    Pokaż uproszczony widok rekordu Zobacz statystyki


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