{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T00:07:10Z","timestamp":1783901230116,"version":"3.55.0"},"reference-count":11,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2020,4,1]],"date-time":"2020-04-01T00:00:00Z","timestamp":1585699200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,4,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>\n                    Timothy Makarios (with Isabelle\/HOL\n                    <jats:sup>1<\/jats:sup>\n                    ) and John Harrison (with HOL-Light\n                    <jats:sup>2<\/jats:sup>\n                    ) shown that \u201cthe Klein-Beltrami model of the hyperbolic plane satisfy all of Tarski\u2019s axioms except his Euclidean axiom\u201d [2],[3],[4, 5].\n                  <\/jats:p>\n                  <jats:p>With the Mizar system [1] we use some ideas taken from Tim Makarios\u2019s 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.<\/jats:p>","DOI":"10.2478\/forma-2020-0002","type":"journal-article","created":{"date-parts":[[2020,6,2]],"date-time":"2020-06-02T04:52:34Z","timestamp":1591073554000},"page":"9-21","source":"Crossref","is-referenced-by-count":0,"title":["Klein-Beltrami model. Part IV"],"prefix":"10.2478","volume":"28","author":[{"given":"Roland","family":"Coghetto","sequence":"first","affiliation":[{"name":"Rue de la Brasserie 5 7100 La Louvi\u00e8re , Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"374","published-online":{"date-parts":[[2020,5,29]]},"reference":[{"key":"2026071215073296016_j_forma-2020-0002_ref_001_w2aab3b7b3b1b6b1ab1ab1Aa","doi-asserted-by":"crossref","unstructured":"[1] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, Karol P\u0105k, 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\u2013279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007\/978-3-319-20615-8_17.10.1007\/978-3-319-20615-8_17","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"2026071215073296016_j_forma-2020-0002_ref_002_w2aab3b7b3b1b6b1ab1ab2Aa","unstructured":"[2] Eugenio Beltrami. Saggio di interpetrazione della geometria non-euclidea. Giornale di Matematiche, 6:284\u2013322, 1868."},{"key":"2026071215073296016_j_forma-2020-0002_ref_003_w2aab3b7b3b1b6b1ab1ab3Aa","doi-asserted-by":"crossref","unstructured":"[3] Eugenio Beltrami. Essai d\u2019interpr\u00e9tation de la g\u00e9om\u00e9trie non-euclid\u00e9enne. In Annales scientifiques de l\u2019\u00c9cole Normale Sup\u00e9rieure. Trad. par J. Ho\u00fcel, volume 6, pages 251\u2013288. Elsevier, 1869.10.24033\/asens.60","DOI":"10.24033\/asens.60"},{"key":"2026071215073296016_j_forma-2020-0002_ref_004_w2aab3b7b3b1b6b1ab1ab4Aa","unstructured":"[4] Karol Borsuk and Wanda Szmielew. Foundations of Geometry. North Holland, 1960."},{"key":"2026071215073296016_j_forma-2020-0002_ref_005_w2aab3b7b3b1b6b1ab1ab5Aa","unstructured":"[5] Karol Borsuk and Wanda Szmielew. Podstawy geometrii. Pa\u0144stwowe Wydawnictwo Naukowe, Warszawa, 1955 (in Polish)."},{"key":"2026071215073296016_j_forma-2020-0002_ref_006_w2aab3b7b3b1b6b1ab1ab6Aa","doi-asserted-by":"crossref","unstructured":"[6] Roland Coghetto. Homography in \ud835\udd49\ud835\udd472. Formalized Mathematics, 24(4):239\u2013251, 2016. doi:10.1515\/forma-2016-0020.10.1515\/forma-2016-0020","DOI":"10.1515\/forma-2016-0020"},{"key":"2026071215073296016_j_forma-2020-0002_ref_007_w2aab3b7b3b1b6b1ab1ab7Aa","doi-asserted-by":"crossref","unstructured":"[7] Roland Coghetto. Klein-Beltrami model. Part I. Formalized Mathematics, 26(1):21\u201332, 2018. doi:10.2478\/forma-2018-0003.10.2478\/forma-2018-0003","DOI":"10.2478\/forma-2018-0003"},{"key":"2026071215073296016_j_forma-2020-0002_ref_008_w2aab3b7b3b1b6b1ab1ab8Aa","doi-asserted-by":"crossref","unstructured":"[8] Roland Coghetto. Klein-Beltrami model. Part III. Formalized Mathematics, 28(1):1\u20137, 2020. doi:10.2478\/forma-2020-0001.10.2478\/forma-2020-0001","DOI":"10.2478\/forma-2020-0001"},{"key":"2026071215073296016_j_forma-2020-0002_ref_009_w2aab3b7b3b1b6b1ab1ab9Aa","unstructured":"[9] Kanchun, Hiroshi Yamazaki, and Yatsuka Nakamura. Cross products and tripple vector products in 3-dimensional Euclidean space. Formalized Mathematics, 11(4):381\u2013383, 2003."},{"key":"2026071215073296016_j_forma-2020-0002_ref_010_w2aab3b7b3b1b6b1ab1ac10Aa","unstructured":"[10] Timothy James McKenzie Makarios. A mechanical verification of the independence of Tarski\u2019s Euclidean Axiom. Victoria University of Wellington, New Zealand, 2012. Master\u2019s thesis."},{"key":"2026071215073296016_j_forma-2020-0002_ref_011_w2aab3b7b3b1b6b1ab1ac11Aa","doi-asserted-by":"crossref","unstructured":"[11] William Richter, Adam Grabowski, and Jesse Alama. Tarski geometry axioms. Formalized Mathematics, 22(2):167\u2013176, 2014. doi:10.2478\/forma-2014-0017.10.2478\/forma-2014-0017","DOI":"10.2478\/forma-2014-0017"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/content.sciendo.com\/view\/journals\/forma\/28\/1\/article-p9.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2020-0002","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,12]],"date-time":"2026-07-12T23:11:27Z","timestamp":1783897887000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2020-0002"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,4,1]]},"references-count":11,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2020,5,29]]},"published-print":{"date-parts":[[2020,4,1]]}},"alternative-id":["10.2478\/forma-2020-0002"],"URL":"https:\/\/doi.org\/10.2478\/forma-2020-0002","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2020,4,1]]}}}