REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

  1. Repozytorium Uniwersytetu w Białymstoku
  2. Czasopisma naukowe / Journals
  3. Formalized Mathematics
  4. Formalized Mathematics, 2017, Volume 25, Issue 4

Szukanie zaawansowane
  • Zespoły i Kolekcje


  • Zaloguj się
  • Zarejestruj się
  • Mój RUB
  • FAQ
  • Polityka
  • Regulamin
  • DOI
  • Instrukcja
  • Aspekty prawne
  • Open Access
  • Archiwum


  • Kontakt
  • O Dspace
  • Strona Biblioteki
  • Strona Uczelni



    • Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/6554
    Pełny rekord metadanych
    Pole DCWartośćJęzyk
    dc.contributor.authorCoghetto, Roland-
    dc.contributor.authorGrabowski, Adam-
    dc.date.accessioned2018-05-11T07:20:22Z-
    dc.date.available2018-05-11T07:20:22Z-
    dc.date.issued2017-
    dc.identifier.citationFormalized Mathematics, Volume 25, Issue 4, Pages 289–313-
    dc.identifier.issn1426-2630-
    dc.identifier.urihttp://hdl.handle.net/11320/6554-
    dc.description.abstractIn 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).-
    dc.language.isoen-
    dc.publisherDeGruyter Open-
    dc.subjectTarski’s geometry axioms-
    dc.subjectfoundations of geometry-
    dc.subjectEuclidean plane-
    dc.titleTarski Geometry Axioms. Part III-
    dc.typeArticle-
    dc.identifier.doi10.1515/forma-2017-0028-
    dc.description.AffiliationCoghetto Roland - Rue de la Brasserie 5, 7100 La Louvière, Belgium-
    dc.description.AffiliationGrabowski Adam - Institute of Informatics, University of Białystok, Poland-
    dc.description.referencesMichael Beeson and Larry Wos. OTTER proofs in Tarskian geometry. In International Joint Conference on Automated Reasoning, volume 8562 of Lecture Notes in Computer Science, pages 495-510. Springer, 2014. doi: 10.1007/978-3-319-08587-6 38.-
    dc.description.referencesGabriel Braun and Julien Narboux. A synthetic proof of Pappus’ theorem in Tarski’s geometry. Journal of Automated Reasoning, 58(2):23, 2017. doi: 10.1007/s10817-016-9374-4.-
    dc.description.referencesRoland Coghetto and Adam Grabowski. Tarski geometry axioms - Part II. Formalized Mathematics, 24(2):157-166, 2016. doi: 10.1515/forma-2016-0012.-
    dc.description.referencesSana Stojanovic Durdevic, Julien Narboux, and Predrag Janičic. Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry. Annals of Mathematics and Artificial Intelligence, 74(3-4):249-269, 2015.-
    dc.description.referencesAdam Grabowski. Tarski’s geometry modelled in Mizar computerized proof assistant. In Maria Ganzha, Leszek Maciaszek, and Marcin Paprzycki, editors, Proceedings of the 2016 Federated Conference on Computer Science and Information Systems (FedCSIS), volume 8 of ACSIS - Annals of Computer Science and Information Systems, pages 373-381, 2016. doi: 10.15439/2016F290.-
    dc.description.referencesHaragauri Narayan Gupta. Contributions to the Axiomatic Foundations of Geometry. PhD thesis, University of California-Berkeley, 1965.-
    dc.description.referencesTimothy James McKenzie Makarios. A mechanical verification of the independence of Tarski’s Euclidean Axiom. Victoria University ofWellington, New Zealand, 2012. Master’s thesis.-
    dc.description.referencesTimothy James McKenzie Makarios. The independence of Tarski’s Euclidean Axiom. Archive of Formal Proofs, October 2012. Formal proof development.-
    dc.description.referencesTimothy James McKenzie Makarios. A further simplification of Tarski’s axioms of geometry. Note di Matematica, 33(2):123-132, 2014.-
    dc.description.referencesJulien Narboux. Mechanical theorem proving in Tarski’s geometry. In F. Botana and T. Recio, editors, Automated Deduction in Geometry, volume 4869 of Lecture Notes in Computer Science, pages 139-156. Springer, 2007.-
    dc.description.referencesWilliam Richter, Adam Grabowski, and Jesse Alama. Tarski geometry axioms. Formalized Mathematics, 22(2):167-176, 2014. doi: 10.2478/forma-2014-0017.-
    dc.description.referencesWolfram Schwabhäuser, Wanda Szmielew, and Alfred Tarski. Metamathematische Methoden in der Geometrie. Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1983.-
    dc.identifier.eissn1898-9934-
    dc.description.volume25-
    dc.description.issue4-
    dc.description.firstpage289-
    dc.description.lastpage313-
    dc.identifier.citation2Formalized Mathematics-
    Występuje w kolekcji(ach):Artykuły naukowe (WInf)
    Formalized Mathematics, 2017, Volume 25, Issue 4

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


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