{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T20:04:50Z","timestamp":1780085090298,"version":"3.54.0"},"reference-count":0,"publisher":"Walter de Gruyter GmbH","issue":"2","license":[{"start":{"date-parts":[[2014,6,30]],"date-time":"2014-06-30T00:00:00Z","timestamp":1404086400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,6,30]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>This is the translation of the Mizar article containing readable Mizar proofs of some axiomatic geometry theorems formulated by the great Polish mathematician Alfred Tarski [8], and we hope to continue this work.<\/jats:p>\n                  <jats:p>The article is an extension and upgrading of the source code written by the first author with the help of miz3 tool; his primary goal was to use proof checkers to help teach rigorous axiomatic geometry in high school using Hilbert\u2019s axioms.<\/jats:p>\n                  <jats:p>This is largely a Mizar port of Julien Narboux\u2019s Coq pseudo-code [6]. We partially prove the theorem of [7] that Tarski\u2019s (extremely weak!) plane geometry axioms imply Hilbert\u2019s axioms. Specifically, we obtain Gupta\u2019s amazing proof which implies Hilbert\u2019s axiom I1 that two points determine a line.<\/jats:p>\n                  <jats:p>The primary Mizar coding was heavily influenced by [9] on axioms of incidence geometry. The original development was much improved using Mizar adjectives instead of predicates only, and to use this machinery in full extent, we have to construct some models of Tarski geometry. These are listed in the second section, together with appropriate registrations of clusters. Also models of Tarski\u2019s geometry related to real planes were constructed.<\/jats:p>","DOI":"10.2478\/forma-2014-0017","type":"journal-article","created":{"date-parts":[[2015,2,5]],"date-time":"2015-02-05T08:48:28Z","timestamp":1423126108000},"page":"167-176","source":"Crossref","is-referenced-by-count":6,"title":["Tarski Geometry Axioms"],"prefix":"10.2478","volume":"22","author":[{"given":"William","family":"Richter","sequence":"first","affiliation":[{"name":"Departament of Mathematics Nortwestern University Evanston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Adam","family":"Grabowski","sequence":"additional","affiliation":[{"name":"Institute of Informatics University of Bia\u0142ystok Akademicka 2, 15-267 Bia\u0142ystok Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jesse","family":"Alama","sequence":"additional","affiliation":[{"name":"Technical University of Vienna Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"374","published-online":{"date-parts":[[2014,6,30]]},"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/22\/2\/article-p167.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2014-0017","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T19:57:31Z","timestamp":1780084651000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2014-0017"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,6,30]]},"references-count":0,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2014,6,30]]},"published-print":{"date-parts":[[2014,6,30]]}},"alternative-id":["10.2478\/forma-2014-0017"],"URL":"https:\/\/doi.org\/10.2478\/forma-2014-0017","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,6,30]]}}}