REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/6554
Tytuł: Tarski Geometry Axioms. Part III
Autorzy: Coghetto, Roland
Grabowski, Adam
Słowa kluczowe: Tarski’s geometry axioms
foundations of geometry
Euclidean plane
Data wydania: 2017
Data dodania: 11-maj-2018
Wydawca: DeGruyter Open
Źródło: Formalized Mathematics, Volume 25, Issue 4, Pages 289–313
Abstrakt: In the article, we continue the formalization of the work devoted to Tarski’s geometry - the book “Metamathematische Methoden in der Geometrie” by W. Schwabhäuser, W. Szmielew, and A. Tarski. After we prepared some introductory formal framework in our two previous Mizar articles, we focus on the regular translation of underlying items faithfully following the abovementioned book (our encoding covers first seven chapters). Our development utilizes also other formalization efforts of the same topic, e.g. Isabelle/HOL by Makarios, Metamath or even proof objects obtained directly from Prover9. In addition, using the native Mizar constructions (cluster registrations) the propositions (“Satz”) are reformulated under weaker conditions, i.e. by using fewer axioms or by proposing an alternative version that uses just another axioms (ex. Satz 2.1 or Satz 2.2).
Afiliacja: Coghetto Roland - Rue de la Brasserie 5, 7100 La Louvière, Belgium
Grabowski Adam - Institute of Informatics, University of Białystok, Poland
URI: http://hdl.handle.net/11320/6554
DOI: 10.1515/forma-2017-0028
ISSN: 1426-2630
e-ISSN: 1898-9934
Typ Dokumentu: Article
Występuje w kolekcji(ach):Artykuły naukowe (WMiI)
Formalized Mathematics, 2017, Volume 25, Issue 4

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2017-0028.pdf359,35 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki


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