REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/7842
Tytuł: Tarski Geometry Axioms. Part IV – Right Angle
Autorzy: Coghetto, Roland
Grabowski, Adam
Słowa kluczowe: Tarski geometry
foundations of geometry
right angle
Data wydania: 2019
Data dodania: 21-maj-2019
Wydawca: DeGruyter Open
Źródło: Formalized Mathematics, Volume 27, Issue 1, Pages 75-85
Abstrakt: In the article, we continue [7] the formalization of the work devoted to Tarski’s geometry – the book “Metamathematische Methoden in der Geometrie” (SST for short) by W. Schwabhäuser, W. Szmielew, and A. Tarski [14], [9], [10]. We use the Mizar system to systematically formalize Chapter 8 of the SST book.We define the notion of right angle and prove some of its basic properties, a theory of intersecting lines (including orthogonality). Using the notion of perpendicular foot, we prove the existence of the midpoint (Satz 8.22), which will be used in the form of the Mizar functor (as the uniqueness can be easily shown) in Chapter 10. In the last section we give some lemmas proven by means of Otter during Tarski Formalization Project by M. Beeson (the so-called Section 8A of SST).
Afiliacja: Roland Coghetto - Rue de la Brasserie 5, 7100 La Louvi`ere, Belgium
Adam Grabowski - Institute of Informatics, University of Białystok, Poland
URI: http://hdl.handle.net/11320/7842
DOI: 10.2478/forma-2019-0008
ISSN: 1426-2630
e-ISSN: 1898-9934
metadata.dc.identifier.orcid: 0000-0002-4901-0766
0000-0001-5026-3990
Typ Dokumentu: Article
Występuje w kolekcji(ach):Artykuły naukowe (WMiI)
Formalized Mathematics, 2019, Volume 27, Issue 1

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma_2019_27_1_008.pdf255,95 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki


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