@MISC{BKMODEL3.MIZ,
    TITLE = {Beltrami-{K}lein model, Part {III}},
    AUTHOR = {Coghetto, Roland},
    ADDRESS1 = {Rue de la Brasserie 5\\7100 La Louvi\`ere, Belgium},
    DAY = {30},
    MONTH = {December},
    YEAR = {2019},
    SUMMARY = {Makarios (with
    Isabelle/HOL\footnote{\url{https://www.isa-afp.org/entries/Tarskis_Geometry.html}})
   and John Harisson (with HOL-Light
   \footnote{\url{https://github.com/jrh13/hol-light/blob/master/100/independence.ml}})
   shown that "the Klein-Beltrami model of the hyperbolic
   plane satisfy all of Tarski's axioms except his Euclidean axiom"
   \cite{beltrami1868saggio,beltrami1869essai,BORSUK:1,BS55}.\par
  With the Mizar system \cite{Mizar-State-2015}
  we use some ideas
  taken from Tim Makarios's MSc thesis\cite{makarios2012mechanical} to
  formalize some definitions (like the absolute) and
  lemmas necessary for the verification of the independence
  of the parallel postulate.},
    MSC2010 = {5103;51A05;51M10;03B35},
    KEYWORDS = {Tarski's geometry axioms; foundations of geometry;
    Beltrami-Klein model}}

@article{makarios2012mechanical,
  title={A Mechanical Verification of the Independence of Tarski's Euclidean Axiom},
  author={Makarios, Timothy James McKenzie},
  year={2012},
  publisher={Victoria University of Wellington}
}

@article{beltrami1868saggio,
  title={Saggio di interpetrazione della geometria non-euclidea},
  author={Beltrami, Eugenio},
  journal={Giornale di Matematiche},
  volume={6},
  pages={284--322},
  year={1868}
}

@inproceedings{beltrami1869essai,
  title={Essai d'interpr{\'e}tation de la g{\'e}om{\'e}trie noneuclid{\'e}enne. Trad. par J. Ho{\"u}el},
  author={Beltrami, Eugenio},
  booktitle={Annales scientifiques de l'{\'E}cole Normale Sup{\'e}rieure},
  volume={6},
  pages={251--288},
  year={1869},
  organization={Elsevier}
}

@book{BS55,
  title={Podstawy geometrii},
  author={Borsuk, Karol and Szmielew, Wanda},
  year={1955},
  publisher={Pa\'nstwowe Wydawnictwo Naukowe,Warsawa}
}

