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/6832
    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 33–48-
    dc.identifier.issn1426-2630-
    dc.identifier.urihttp://hdl.handle.net/11320/6832-
    dc.description.abstractTim 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].-
    dc.language.isoen-
    dc.publisherDeGruyter Open-
    dc.subjectTarski’s geometry axioms-
    dc.subjectfoundations of geometry-
    dc.subjectKlein-Beltrami model-
    dc.titleKlein-Beltrami Model. Part II-
    dc.typeArticle-
    dc.identifier.doi10.2478/forma-2018-0004-
    dc.description.AffiliationRue de la Brasserie 5, 7100 La Louvière, Belgium-
    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.referencesRoland Coghetto. Homography in ℝℙ2. Formalized Mathematics, 24(4):239–251, 2016. doi:10.1515/forma-2016-0020.-
    dc.description.referencesRoland Coghetto. Group of homography in real projective plane. Formalized Mathematics, 25(1):55–62, 2017. doi:10.1515/forma-2017-0005.-
    dc.description.referencesRoland Coghetto. Klein-Beltrami model. Part I. Formalized Mathematics, 26(1):21–32, 2018. doi:10.2478/forma-2018-0003.-
    dc.description.referencesRoland Coghetto. Pascal’s theorem in real projective plane. Formalized Mathematics, 25 (2):107–119, 2017. doi:10.1515/forma-2017-0011.-
    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.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.referencesYatsuka Nakamura. Graph theoretical properties of arcs in the plane and Fashoda Meet Theorem. Formalized Mathematics, 7(2):193–201, 1998.-
    dc.description.referencesKarol Pąk and Andrzej Trybulec. Laplace expansion. Formalized Mathematics, 15(3): 143–150, 2007. doi:10.2478/v10037-007-0016-5.-
    dc.description.referencesAndrzej Trybulec. A Borsuk theorem on homotopy types. Formalized Mathematics, 2(4): 535–545, 1991.-
    dc.identifier.eissn1898-9934-
    dc.description.volume26-
    dc.description.issue1-
    dc.description.firstpage33-
    dc.description.lastpage48-
    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-0004.pdf310,35 kBAdobe PDFOtwórz
    Pokaż uproszczony widok rekordu Zobacz statystyki


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