Uneingeschränkter Zugang

Klein-Beltrami Model. Part II

   | 28. Juli 2018

Zitieren

Tim Makarios (with Isabelle/HOL1) and John Harrison (with HOL-Light2) have shown that “the Klein-Beltrami model of the hyperbolic plane satisfy all of Tarski’s axioms except his Euclidean axiom” [2, 3, 15, 4].

With the Mizar system [1], [10] we use some ideas are taken from Tim Makarios’ MSc thesis [12] for formalized some definitions (like the tangent) and lemmas necessary for the verification of the independence of the parallel postulate. This work can be also treated as a further development of Tarski’s geometry in the formal setting [9].

eISSN:
1898-9934
ISSN:
1426-2630
Sprache:
Englisch
Zeitrahmen der Veröffentlichung:
4 Hefte pro Jahr
Fachgebiete der Zeitschrift:
Informatik, andere, Mathematik, Allgemeines