Marek Janasz UP Cracow
   Thesis: Automated theorem proving for elementary geometry.

   This study analyses automated proofs of theorems from Euclidean Ele-
ments, book VI, using the area method. The theorems we will be discussing
concern Euclidean field theory about equality of non-congruent figures and
similarity of the figures [1]. The proofs are generated by the program
WinGCLC.
   My proposed hypothesizes:
   1. The way of modification of the elimination lemmas while adding the
      elementary constructions to extending the abilities of the area method
      in proving theorems from Euclidean Elements, book VI.
   2. The method of extension of the axiomatic system from [5] to proving
      theorem for ordered geometry.
    I would like to use my results to implement the prover to the programming
languages in logic (Prolog, Haskell) or to the applications like Coq. My dis-
sertation plans contain the analysis of the automated proofs of segment’s field
from Cartesian arithmetic using the area method by the program WinGCLC.
My study is concerned with proving equality of line segments using various
methods of constructions corresponding with multiplication of line segments
(uniqueness) and commutative property of multiplication of line segments.

   Bibliography:
   1. B laszczyk P., Mrówka K., Euklides Elementy. Ksiegi V-VI teoria propor-
      cji i podobieństwa, t lumaczenie i komentarz, Copernicus Center Press,
      Kraków 2013 (in polish)
   2. B laszczyk P., Mrówka K., Kartezjusz. Geometria, Universitas, Kraków
      2015 (in polish)
   3. Chou S. C. , Gao X. S., Zhang J. Z., Machine Proofs in Geometry, World
      Scientific, Singapore 1994.
   4. Euclid, Elements, edited, and provided with a modern English transla-
      tion, by R. Fitzpatrick;
      http://farside.ph.utexas.edu/Books/ Euclid/Elements.pdf.
   5. Janičić P., Narboux J., Quaresma P., The area method, Journal of Auto-
      mated Reasoning 48, 4 (2012), 489-532.


                                      1