A. B. It-holds-that-a-=-b-or, Assume that: A = B. 6. From the fact(s) AD ? = AB and A = B it holds that AD ? = AA. 7. From the fact(s) AD ? = AA

. Assume, It holds that A = C or A = C. 12 Assume that: A = C. 13. From the fact(s) bet(A, B, C) and A = C it holds that bet(A, B, A). 14. From the fact(s) bet(A, B, A) and bet(B, A, A) it holds that A = B

=. C. Assume, A. , C. Cd, and A. Ad, From the fact(s) A = C it holds that C = A. 18. From the fact(s) C = A and col

J. Avigad, E. Dean, and J. Mumma, A FORMAL SYSTEM FOR EUCLID???S ELEMENTS, The Review of Symbolic Logic, vol.I???III, issue.04, pp.700-768, 2009.
DOI : 10.1007/s10817-007-9071-4

M. Beeson, Proof and Computation in Geometry, Lecture Notes in Computer Science, vol.7993, pp.1-30, 2013.
DOI : 10.1007/978-3-642-40672-0_1

M. Beeson and L. Wos, OTTER Proofs in Tarskian Geometry, Automated Reasoning -7th International Joint Conference, IJCAR 2014, pp.495-510, 2014.
DOI : 10.1007/978-3-319-08587-6_38

J. C. Blanchette, Redirecting proofs by contradiction In: Third International Workshop on Proof Exchange for Theorem Proving, EasyChair, vol.14, pp.11-26, 2013.

M. Bezem and T. Coquand, Automating Coherent Logic, 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning ? LPAR 2005, 2005.
DOI : 10.1007/11591191_18

M. Bezem and D. Hendriks, On the Mechanization of the Proof of Hessenberg???s Theorem in Coherent Logic, Journal of Automated Reasoning, vol.19, issue.1, 2008.
DOI : 10.1007/s10817-007-9086-x

J. C. Blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT Solvers, J. Autom. Reason, vol.37, issue.1-2, pp.109-128, 2013.
DOI : 10.1007/BFb0028402

J. C. Blanchette, L. Bulwahn, and T. Nipkow, Automatic Proof and Disproof in Isabelle/HOL, Frontiers of Combining Systems, 8th International Symposium , Proceedings, volume 6989 of Lecture Notes in Computer Science, pp.12-27
DOI : 10.1007/BFb0028402

P. Boutry, J. Narboux, P. Schreck, and G. Braun, A short note about case distinctions in Tarski's geometry. 10th International Workshop on Automated Deduction in Geometry, pp.51-66, 2014.

P. Boutry, J. Narboux, P. Schreck, and G. Braun, Using small scale automation to improve both accessibility and readability of formal proofs in geometry, 10th International Workshop on Automated Deduction in Geometry, pp.31-50, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00989781

G. Braun and J. Narboux, From Tarski to Hilbert, Lecture Notes in Computer Science, vol.7993, pp.89-109, 2013.
DOI : 10.1007/978-3-642-40672-0_7
URL : https://hal.archives-ouvertes.fr/hal-00727117

J. Fisher and M. Bezem, Skolem Machines and Geometric Logic, Lecture Notes in Computer Science, vol.4711, 2007.
DOI : 10.1007/978-3-540-75292-9_14

M. Ganesalingam and W. T. Gowers, A fully automatic problem solver with humanstyle output. CoRR, abs/1309, p.4501, 2013.

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A Machine-Checked Proof of the Odd Order Theorem, 4th Conference on Interactive Theorem Proving ? ITP 2013, pp.163-179, 2013.
DOI : 10.1007/978-3-642-39634-2_14
URL : https://hal.archives-ouvertes.fr/hal-00816699

H. N. Gupta, Contributions to the axiomatic foundations of geometry, 1965.

T. C. Hales, Introduction to the Flyspeck project, Mathematics, Algorithms , Proofs, volume 05021 of Dagstuhl Seminar Proceedings. Internationales Begegnungs-und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, 2006.

D. Hilbert, Grundlagen der Geometrie, Leipzig, 1899.

C. Kaliszyk and J. Urban, Learning-assisted automated reasoning with Flyspeck. CoRR, abs/1211, p.7012, 2012.

T. Makarios, A further simplification of Tarski's axioms of geometry. CoRR, abs/1306, p.66, 2013.

L. Meikle and J. Fleuriot, Formalizing Hilbert???s Grundlagen in Isabelle/Isar, Theorem Proving in Higher Order Logics, pp.319-334, 2003.
DOI : 10.1007/10930755_21

L. Meikle and J. Fleuriot, Mechanical Theorem Proving in Computational Geometry, Lecture Notes in Computer Science, vol.3763, pp.1-18, 2005.
DOI : 10.1007/11615798_1

J. Narboux, Mechanical Theorem Proving in Tarski???s Geometry, Proceedings of Automatic Deduction in Geometry 06, pp.139-156, 2007.
DOI : 10.1007/978-3-540-77356-6_9

A. Polonsky, Proofs, Types and Lambda Calculus, 2011.

A. Quaife, Automated development of Tarski's geometry, Journal of Automated Reasoning, vol.5, issue.1, pp.97-118, 1989.
DOI : 10.1007/BF00245024

A. Riazanov and A. Voronkov, The design and implementation of Vampire, AI Communications, vol.15, issue.2-3, pp.91-110, 2002.

J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, vol.12, issue.1, pp.23-41, 1965.
DOI : 10.1145/321250.321253

S. Schulz, E -a brainiac theorem prover, AI Commun, vol.15, issue.2-3, pp.111-126, 2002.

W. Schwabhuser, W. Szmielew, and A. Tarski, Metamathematische Methoden in der Geometrie, 1983.
DOI : 10.1007/978-3-642-69418-9

S. Stojanovi´cstojanovi´c, J. Narboux, M. Bezem, and P. Jani?i´jani?i´c, A Vernacular for Coherent Logic, Conferences on Intelligent Computer Mathematics, pp.388-403, 2014.
DOI : 10.1007/978-3-319-08434-3_28

S. Stojanovi´cstojanovi´c, V. Pavlovi´cpavlovi´c, and P. Jani?i´jani?i´c, A coherent logic based geometry theorem prover capable of producing formal and readable proofs, In: Automated Deduction in Geometry Lecture Notes in Computer Science, vol.6877, 2011.

G. Sutcliffe, The TPTP Problem Library and Associated Infrastructure, Journal of Automated Reasoning, vol.13, issue.2, pp.337-362, 2009.
DOI : 10.1007/s10817-009-9143-8

C. Tankink, C. Kaliszyk, J. Urban, and H. Geuvers, Communicating Formal Proofs: The Case of Flyspeck, Interactive Theorem Proving -4th International Conference , Proceedings, volume 7998 of Lecture Notes in Computer Science, pp.451-456
DOI : 10.1007/978-3-642-39634-2_32

A. Tarski, What is elementary geometry? The axiomatic Method, with special reference to Geometry and Physics, pp.16-29, 1959.

A. Tarski and S. Givant, Abstract, Bulletin of Symbolic Logic, vol.I, issue.02, 1999.
DOI : 10.1090/S0002-9947-1902-1500592-8

C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda et al., SPASS Version 3.5, Spass version 3.5. In: Automated Deduction -CADE-22 Proceedings, pp.140-145, 2009.
DOI : 10.1007/978-3-540-73595-3_38

M. Wenzel, Isar ??? A Generic Interpretative Approach to Readable Formal Proof Documents, Theorem Proving in Higher Order Logics (TPHOLs'99), volume 1690 of Lecture Notes in Computer Science, pp.167-184, 1999.
DOI : 10.1007/3-540-48256-3_12
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.3203

F. Wiedijk, The seventeen provers of the World, Lecture Notes in Computer Science, vol.3600, 2006.
DOI : 10.1007/11542384