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 (WInf) Formalized Mathematics, 2019, Volume 27, Issue 1 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma_2019_27_1_008.pdf | 255,95 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL