REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/3713
Tytuł: Tarski Geometry Axioms
Autorzy: Richter, William
Grabowski, Adam
Alama, Jesse
Słowa kluczowe: Tarski’s geometry axioms
foundations of geometry
incidence geometry
Data wydania: 2014
Data dodania: 9-gru-2015
Wydawca: De Gruyter Open
Źródło: Formalized Mathematics, Volume 22, Issue 2, 2014, Pages 167-176
Abstrakt: 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. 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’s axioms. This is largely a Mizar port of Julien Narboux’s Coq pseudo-code [6]. We partially prove the theorem of [7] that Tarski’s (extremely weak!) plane geometry axioms imply Hilbert’s axioms. Specifically, we obtain Gupta’s amazing proof which implies Hilbert’s axiom I1 that two points determine a line. 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’s geometry related to real planes were constructed.
Afiliacja: Richter William - Departament of Mathematics Nortwestern University Evanston, USA
Grabowski Adam - Institute of Informatics University of Białystok Akademicka 2, 15-267 Białystok Poland
Alama Jesse - Technical University of Vienna Austria
URI: http://hdl.handle.net/11320/3713
DOI: 10.2478/forma-2014-0017
ISSN: 1426-2630
1898-9934
Typ Dokumentu: Article
Występuje w kolekcji(ach):Artykuły naukowe (WMiI)
Formalized Mathematics, 2014, Volume 22, Issue 2

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2014-0017.pdf244,25 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki


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