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 (WInf) Formalized Mathematics, 2017, Volume 25, Issue 4 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma-2017-0028.pdf | 359,35 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL