@MISC{GTARSKI2.MIZ,
  AUTHOR = {Coghetto, Roland and Grabowski, Adam},
  TITLE = {Tarski Geometry Axioms -- Part {II}},
  SECTION1 = {Preliminaries},
  SECTION2 = {Basic Properties of the Euclidean Plane},
  SECTION3 = {Ordered Affine Space Generated by \verb!TOP-REAL 2!},
  SECTION4 = {Eucldiean Plane Satisfies First 7 Tarski's Axioms},
  SECTION5 = {Preparation for The Rest of Tarski's Axioms},
  SECTION6 = {Four Remaining Axioms of Tarski},
  SECTION7 = {Axiom A11 -- Axiom Schema of Continuity},
  SECTION8 = {Corrolaries},
  DAY = {30},
  MONTH = {June},
  YEAR = {2016},
  ADDRESS1 = {Rue de la Brasserie 5\\7100 La Louvi\`ere, Belgium},
  ADDRESS2 = {Institute of Informatics\\University of Bia{\l}ystok\\
  ul. Konstantego Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok, Poland},
  SUMMARY = {In our earlier Mizar article \cite{GTARSKI1.ABS},
    the first part of axioms of geometry due to Alfred Tarski
    \cite{TarskiGivant}, was formally introduced.
    We defined a structure \verb!TarskiPlane! with the following predicates:
    \begin{itemize}
    \item of betweenness \verb!between! (a ternary relation),
    \item of \verb!equiv! (quarternary relation),
    \item of congruence \verb!cong! (relation with 6 arguments),
    \end{itemize}
    \noindent
    which satisfy the following properties:
    \begin{itemize}
    \item congruence symmetry (A1),
    \item congruence equivalence relation (A2),
    \item congruence identity (A3),
    \item segment construction (A4),
    \item SAS (A5),
    \item betweenness identity (A6),
    \item Pasch (A7).
    \end{itemize}
    Also a simple model, which satisfies these axioms,
    was previosly constructed. In this paper, we deal with four
    remaining axioms, namely:
    \begin{itemize}
    \item the lower dimension axiom (A8),
    \item the upper dimension axiom (A9),
    \item the Euclid axiom (A10),
    \item the continuity axiom (A11).
    \end{itemize}
    They were introduced in the form of Mizar attributes.
    \par
    In order to show that the structure which satisfies all eleven
    Tarski's axioms really exists, we provided a proof of the registration
    of a cluster that the Euclidean plane, or rather
    a natural extension of ordinary metric structure \verb!Euclid 2!
    satisfies all these attributes.
    \par
    Connection with Isabelle should be mentioned -- we had some doubts about
    the proof of the Euclid's axiom and inspection of the proof taken from
    Archive of Formal Proofs clarified things a bit.}}

@BOOK{Schwabhauser:1983,
 AUTHOR = {Schwabh\"auser, Wolfram and Szmielew, Wanda and Tarski, Alfred},
 TITLE = {Metamathematische Methoden in der Geometrie},
 YEAR = {1983},
 PUBLISHER = {Springer-Verlag, Berlin, Heidelberg, New York, Tokyo}}

@INPROCEEDINGS{Narboux:2007,
       AUTHOR = {Narboux, Julien},
        TITLE = {Mechanical theorem proving in Tarski's geometry},
      JOURNAL = {Lecture Notes in Computer Science},
      BOOKTITLE = {Automated Deduction in Geometry},
      EDITOR = {F. Botana and T. Recio},
         YEAR = {2007},
       VOLUME = {4869},
        PAGES = {139--156}}

@ARTICLE{TarskiGivant,
 AUTHOR = {Tarski, Alfred and Givant, Steven},
 TITLE = {Tarski's system of geometry},
 JOURNAL = {Bulletin of Symbolic Logic},
 YEAR = 1999,
 VOLUME = 5,
 NUMBER = 2,
 PAGES={175--214}}
