J. Avigad, E. Dean, and J. Mumma, A formal system for Euclid's Elements. The Review of Symbolic Logic, 2009.

M. Beeson, Proof and Computation in Geometry, Automated Deduction in Geometry -9th International Workshop
DOI : 10.1007/978-3-642-40672-0_1

V. Marinkovic, P. Janicic, and P. Schreck, Computer Theorem Proving for Verifiable Solving of Geometric Construction Problems, Automated Deduction in Geometry -10th International Workshop, Revised Selected Papers, pp.72-93, 2015.
DOI : 10.1007/978-3-319-21362-0_5

V. Marinkovi´cmarinkovi´c and P. Jani?i´jani?i´c, Towards Understanding Triangle Construction Problems, Intelligent Computer Mathematics -CICM 2012, 2012.

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

M. Nikoli´cnikoli´c and P. Jani?i´jani?i´c, CDCL-based abstract state transition system for coherent logic, Lecture Notes in Computer Science, vol.7362, 2012.

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle HOL: a Proof Assistant for Higher-Order Logic, 2005.
DOI : 10.1007/3-540-45949-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, pp.91-110, 2002.

S. Schulz, E -a brainiac theorem prover, AI Communications, 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. Stojanovic, J. Narboux, M. Bezem, and P. Janicic, A Vernacular for Coherent Logic, Intelligent Computer Mathematics, pp.388-403, 2014.
DOI : 10.1007/978-3-319-08434-3_28

URL : https://hal.archives-ouvertes.fr/hal-00983975

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, Automated Deduction in Geometry, 2011.

A. Tarski and S. Givant, Tarski's system of geometry. The Bulletin of Symbolic Logic, 1999.

S. Vickers, Geometric Logic in Computer Science, Theory and Formal Methods , Workshops in Computing, pp.37-54, 1993.
DOI : 10.1007/978-1-4471-3503-6_4

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

W. Wernick, Triangle Constructions with Three Located Points, Mathematics Magazine, vol.55, issue.4, pp.227-230, 1982.
DOI : 10.2307/2690164

F. Wiedijk, H. Vernacular-barki, J. M. Cane, L. Garnier, D. Michelucci et al., Unpublished note Solving the pentahedron problem, Computer-Aided Design, vol.58, pp.200-209, 2000.

G. Gouaty, L. Fang, D. Michelucci, M. Daniel, J. P. Pernot et al., Variational geometric modeling with black box constraints and DAGs, Computer-Aided Design, vol.75, issue.76, pp.1-12, 2016.
DOI : 10.1016/j.cad.2016.02.002

URL : https://hal.archives-ouvertes.fr/hal-01281351

D. Michelucci, An epsilon-arithmetic for removing degeneracies, 12th Symposium on Computer Arithmetic. p. 230, 1995.

J. Alama and V. Pambuccian, From absolute to affine geometry in terms of pointreflections , midpoints, and collinearity, pp.11-24, 2016.

D. Barbilian, ExkursüberExkurs¨Exkursüber die Dreiecke, Bulletin Mathématique de la Société des Sciences Mathématiques de Roumanie, vol.38, pp.3-62, 1936.

V. Pambuccian, Zum Stufenaufbau des Parallelenaxioms, Journal of Geometry, vol.18, issue.1-2, pp.79-88, 1994.
DOI : 10.1007/BF01226859

URL : http://deepblue.lib.umich.edu/bitstream/2027.42/43033/1/22_2005_Article_BF01226859.pdf

V. Pambuccian, The Erd??s-Mordell inequality is equivalent to non-positive curvature, Journal of Geometry, vol.88, issue.1-2, pp.134-139, 2008.
DOI : 10.1007/s00022-007-1961-4

V. Pambuccian, On the equivalence of Lagrange???s axiom to the Lotschnittaxiom, Journal of Geometry, vol.143, issue.1-2, pp.165-171, 2009.
DOI : 10.1007/s00022-009-0018-2

V. Pambuccian, On a paper of Dan Barbilian, Note di Matematica, vol.29, pp.29-31, 2009.

W. Szmielew, The Pasch axiom as a consequence of the circle axiom, Bulletin de l'Académie Polonaise des Sciences, Série des Sciences Mathématiques, Astronomiques et Physiques, pp.751-758, 1970.

R. 1. Botana, M. Hohenwarter, P. Jani?i?, Z. Kovács, I. Petrovi? et al., Automated Theorem Proving in GeoGebra: Current Achievements, Journal of Automated Reasoning, vol.74, issue.3, pp.39-59, 2015.
DOI : 10.1007/s10817-015-9326-4

R. 1. Agarwal, B. Aronov, J. O-'rourke, and C. A. Schevon, Star Unfolding of a Polytope with Applications, SIAM Journal on Computing, vol.26, issue.6, pp.1689-1713, 1997.
DOI : 10.1137/S0097539793253371

M. A. Alam and I. Streinu, Star unfolding polygons Automated Deduction in Geometry (ADG'14, Lecture Notes in Artificial Intelligence Lecture Notes in Artificial Intelligence, vol.9201, issue.9201, pp.1-20, 2014.

A. D. Alexandrov, Convex Polyhedra English Translation of Russian edition, Gosudarstv. Izdat.Tekhn.-Teor.Lit, 1950.

A. D. Chapman, /. Hill, T. Crc, and F. Group, Intrinsic Geometry of Convex Surfaces, 2006.

B. Aronov and J. O-'rourke, Nonoverlap of the star unfolding, Discrete & Computational Geometry, vol.15, issue.3, pp.219-250, 1992.
DOI : 10.1007/BF02293047

E. D. Demaine and J. O-'rourke, Geometric Folding Algorithms: Linkages, Origami, and Polyhedra, 2007.
DOI : 10.1017/CBO9780511735172

K. Fukuda, Strange unfoldings of convex polytopes, 1997.

E. Miller and I. Pak, Metric Combinatorics of Convex Polyhedra: Cut Loci and Nonoverlapping Unfoldings, Discrete & Computational Geometry, vol.11, issue.3, pp.339-388, 2008.
DOI : 10.1007/s00454-008-9052-3

D. Mount, On finding shortest path on convex polyhedra, 1985.

W. Schlickenrieder, Nets of polyhedra, 1997.

M. Sharir and A. Schorr, On Shortest Paths in Polyhedral Spaces, SIAM Journal on Computing, vol.15, issue.1, pp.193-215, 1986.
DOI : 10.1137/0215014

W. H. Baur and R. X. Fischer, A historical note on the sodalite framework: The contribution of Frans Maurits Jaeger, Microporous and Mesoporous Materials, vol.116, issue.1-3, pp.1-3, 2008.
DOI : 10.1016/j.micromeso.2008.04.005

C. S. Borcea and I. Streinu, Periodic frameworks and flexibility, Proc. Roy. Soc. A, pp.2633-2649, 2010.
DOI : 10.1073/pnas.16.7.453

C. S. Borcea and I. Streinu, Deformations of crystal frameworks, 2011.

C. S. Borcea and I. Streinu, Frameworks with crystallographic symmetry, Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, vol.113, issue.7-8, 2014.
DOI : 10.1107/S0108767310042832

W. Depmeier, The Sodalite Family - A Simple but Versatile Framework Structure, Reviews in Mineralogy and Geochemistry, vol.57, issue.1, pp.203-240, 2005.
DOI : 10.2138/rmg.2005.57.7

M. T. Dove, Theory of displacive phase transitions in minerals, American Mineralogist, vol.82, issue.3-4, pp.213-244, 1997.
DOI : 10.2138/am-1997-3-401

R. X. Fischer and W. H. Baur, Symmetry relationships of sodalite (SOD) ??? type crystal structures, Zeitschrift f??r Kristallographie, vol.224, issue.4, pp.185-197, 2009.
DOI : 10.1524/zkri.2009.1147

I. Hassan and H. D. Grundy, The crystal structures of sodalite-group minerals, Acta Crys, B40, pp.6-13, 1984.

M. Kotani and T. Sunada, Standard realizations of crystal lattices via harmonic maps, Transactions of the American Mathematical Society, vol.353, issue.01, pp.1-20, 2000.
DOI : 10.1090/S0002-9947-00-02632-5

O. 'keeffe and M. , N-dimensional diamond, sodalite and rare sphere packings, Acta Crystallographica Section A Foundations of Crystallography, vol.47, issue.6, pp.748-753, 1991.
DOI : 10.1107/S0108767391006633

L. Pauling, The structure of sodalite and helvite, Z. Kristallogr, vol.74, pp.213-225, 1930.

D. Taylor, The thermal expansion behaviour of the framework silicates, Mineralogical Mag, pp.593-604, 1972.

W. Thompson, On the Division of Space with Minimum Partitional Area, Philosophical Magazine, vol.24, issue.503, p.10, 1080.

D. Weaire and R. Phelan, A counter-example to Kelvin's conjecture on minimal surfaces, Philosophical Magazine Letters, vol.25, issue.2, p.1009500839408241577, 1080.
DOI : 10.1126/science.161.3838.276

O. Aichholzer, D. Alberts, F. Aurenhammer, and B. Gärtner, A Novel Type of Skeleton for Polygons, Journal of Universal Computer Science, vol.1, issue.12, pp.752-761, 1995.
DOI : 10.1007/978-3-642-80350-5_65

T. Biedl, M. Held, S. Huber, D. Kaaser, and P. Palfrader, Straight skeletons of monotone polygons, 30th (EuroCG '14), 2014.

J. C. Bowers and I. Streinu, Rigidity of Origami Universal Molecules, Automated Deduction in Geometry, pp.120-142, 2012.
DOI : 10.1007/978-3-642-40672-0_9

S. Cheng, L. Mencel, and A. Vigneron, A faster algorithm for computing straight skeletons, Proc. 22nd Euro. Symp. on Algorithms, 2014.

S. W. Cheng and A. Vigneron, Motorcycle Graphs and Straight Skeletons, Proc. 13th Symp. on Discrete algorithms, SODA '02, pp.156-165, 2002.
DOI : 10.1007/s00453-006-1229-7

E. D. Demaine and M. L. Demaine, Computing extreme origami bases, 1997.

S. Huber and M. Held, Theoretical and practical results on straight skeletons of planar straight-line graphs, Proceedings of the 27th annual ACM symposium on Computational geometry, SoCG '11, pp.171-178, 2011.
DOI : 10.1145/1998196.1998223

R. J. Lang, A computational algorithm for origami design, Proceedings of the twelfth annual symposium on Computational geometry , SCG '96, pp.98-105, 1996.
DOI : 10.1145/237218.237249

A. Vigneron and L. Yan, A faster algorithm for computing motorcycle graphs, Proceedings of the 29th annual symposium on Symposuim on computational geometry, SoCG '13, pp.17-26, 2013.
DOI : 10.1145/2462356.2462396

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

. Buekenhout, Francis: Handbook of Incidence Geometry: buildings and foundations, 1995.

P. Castéran and M. Sozeau, A Gentle Introduction to Type Classes and Relations in Coq, 2016.

H. S. Coxeter and . Macdonald, Projective Geometry, 2003.

C. Dehlinger, J. Dufourd, and P. Schreck, Higher- Order Intuitionistic Formalization and Proofs in Hilbert's Elementary Geometry. Automated Deduction in Geometry pp, pp.306-324, 2000.

J. Duprat, Une axiomatique de la géométrie plane en Coq Journées Francophones des Langages Applicatifs pp, pp.123-136, 2008.

L. Fuchs and L. Thery, A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry, Automated Deduction in Geometry, vol.16, issue.5-6, pp.51-67, 2010.
DOI : 10.1007/978-3-7091-4368-1

URL : https://hal.archives-ouvertes.fr/hal-00657901

J. Génevaux, J. Narboux, and S. , Formalization of Wu???s Simple Method in Coq, Certified Programs and Proofs, vol.21, issue.2, pp.71-86, 2011.
DOI : 10.1007/978-3-642-21046-4_10

F. Guilhot, Formalisation en Coq et visualisation d'un cours de g??om??trie pour le lyc??e, Techniques et sciences informatiques, vol.24, issue.9, p.15, 2004.
DOI : 10.3166/tsi.24.1113-1138

P. Jani?i´jani?i´c, J. Narboux, and P. Quaresma, The Area Method, Journal of Automated Reasoning, vol.13, issue.3, pp.489-532, 2012.
DOI : 10.1007/s10817-010-9209-7

C. Jermann, G. Trombettoni, B. Neveu, and P. Mathis, DECOMPOSITION OF GEOMETRIC CONSTRAINT SYSTEMS: A SURVEY, International Journal of Computational Geometry & Applications, vol.16, issue.05n06, pp.379-414, 2006.
DOI : 10.1142/S0218195906002105

URL : https://hal.archives-ouvertes.fr/hal-00481267

G. Kahn, Constructive geometry according to, 1995.

E. Kusak, Desargues theorem in projective 3-space, J. of Formalized Mathematics, vol.2, 1990.

. Lescuyer, Stéphane: First-Class Containers in Coq, Stud. Inform. Univ, vol.9, issue.1, pp.87-127, 2011.

H. Li and Y. Wu, Automated short proof generation for projective geometric theorems with Cayley and bracket algebras, Journal of Symbolic Computation, vol.36, issue.5, pp.717-762, 2003.
DOI : 10.1016/S0747-7171(03)00067-1

N. Magaud, J. Narboux, and P. Schreck, Formalizing Projective Plane Geometry in Coq, Automated Deduction in Geometry, vol.6301, pp.141-162, 2008.
DOI : 10.1007/978-3-642-21046-4_7

URL : https://hal.archives-ouvertes.fr/inria-00305998

N. Magaud, J. Narboux, and P. Schreck, Formalizing Desargues' theorem in Coq using ranks, Proceedings of the 2009 ACM symposium on Applied Computing, SAC '09, pp.1110-1115, 2009.
DOI : 10.1145/1529282.1529527

URL : https://hal.archives-ouvertes.fr/inria-00335719

N. Magaud, J. Narboux, and P. Schreck, A case study in formalizing projective geometry in Coq: Desargues theorem, Computational Geometry, vol.45, issue.8, pp.406-424, 2012.
DOI : 10.1016/j.comgeo.2010.06.004

URL : https://hal.archives-ouvertes.fr/inria-00432810

L. I. Meikle and J. D. Fleuriot, Formalizing Hilbert???s Grundlagen in Isabelle/Isar, Theorem proving in higher logics 2758, pp.319-334, 2003.
DOI : 10.1007/10930755_21

D. Michelucci and P. Schreck, Detecting induced incidences in the projective plane, Citeseer, 2004.

D. Michelucci, . Foufou, . Sebti, . Lamarque, and S. Loic, Geometric constraints solving:some tracks, ACM pp, pp.185-196, 2006.
DOI : 10.1145/1128888.1128915

D. Michelucci and P. Schreck, INCIDENCE CONSTRAINTS: A COMBINATORIAL APPROACH, International Journal of Computational Geometry & Applications, vol.16, issue.05n06, pp.443-460, 2006.
DOI : 10.1142/S0218195906002130

F. Moulton and . Ray, A simple non-Desarguesian plane geometry, Transactions of the American Mathematical Society, vol.3, issue.2, pp.192-195, 1902.
DOI : 10.1090/S0002-9947-1902-1500595-3

J. Narboux, A Decision Procedure for Geometry in Coq, Theorem Proving in Higher Order Logics, pp.225-240, 2004.
DOI : 10.1007/978-3-540-30142-4_17

URL : https://hal.archives-ouvertes.fr/inria-00001035

J. Narboux, Formalisation et automatisation du raisonnement géométrique en Coq, 2006.

J. Narboux, Mechanical Theorem Proving in Tarski's Geometry. Automated Deduction in Geometry 4869, pp.139-156, 2006.

. Richter-gebert, Mechanical theorem proving in projective geometry, Annals of Mathematics and Artificial Intelligence, vol.28, issue.1-2, pp.139-172, 1995.
DOI : 10.1007/BF01531327

M. Sozeau and O. , Nicolas: First-class type classes, Theorem Proving in Higher Order Logics, pp.278-293, 2008.

M. Beeson, CONSTRUCTIVE GEOMETRY, Proceedings of the 10th Asian Logic Conference, 2010.
DOI : 10.1142/9789814293020_0002

M. Beeson, A constructive version of Tarski's geometry. Annals of Pure and Applied Logic, pp.1199-1273, 2015.

M. Beeson and L. Wos, OTTER Proofs in Tarskian Geometry, 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic Proceedings, pp.495-510, 2014.
DOI : 10.1007/978-3-319-08587-6_38

J. Narboux, Mechanical Theorem Proving in Tarski???s Geometry, Lecture Notes in Computer Science, vol.4869, pp.139-156, 2006.
DOI : 10.1007/978-3-540-77356-6_9

W. Richter, Formalizing Rigorous Hilbert Axiomatic Geometry Proofs in the Proof Assistant Hol Light

A. Rosenthal, Vereinfachungen des Hilbertschen Systems der Kongruenzaxiome, Mathematische Annalen, vol.3, issue.2, pp.257-274, 1911.
DOI : 10.1007/BF01456653

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

P. Scott, Mechanising Hilbert's Foundations of Geometry in Isabelle, 2008.

P. Scott and J. Fleuriot, Compass-free Navigation of Mazes, SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science, pp.143-155, 2016.

P. Scott and J. D. Fleuriot, An Investigation of Hilbert???s Implicit Reasoning through Proof Discovery in Idle-Time, Automated Deduction in Geometry -8th International Workshop, ADG 2010, pp.182-200, 2010.
DOI : 10.1007/3-540-44755-5_26

P. Scott and J. D. Fleuriot, A Combinator Language for Theorem Discovery, Intelligent Computer Mathematics -11th International Conference 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012. Proceedings, pp.371-385, 2012.
DOI : 10.1007/978-3-642-31374-5_25

A. Tarski and S. Givant, Tarski's System of Geometry. The bulletin of Symbolic Logic, References 1. Bézier, P.: Courbe et surface. 2` eme edn, pp.175-214, 1986.

L. Garnier, Mathématiques pour la modélisation géométrique, la représentation 3D et la synthèse d'images, Ellipses, pp.978-980, 2007.

J. P. Bécar, Forme (BR) des coniques et de leurs faisceaux, 1997.

J. C. Fiorot and P. Jeannin, Courbes et surfaces rationnelles, 1989.

G. Albrecht, Mathematical methods for curves and surfaces, pp.15-24, 2001.

R. N. Goldman and W. Wang, USING INVARIANTS TO EXTRACT GEOMETRIC CHARACTERISTICS OF CONIC SECTIONS FROM RATIONAL QUADRATIC PARAMETERIZATIONS, International Journal of Computational Geometry & Applications, vol.14, issue.03, pp.161-187, 2004.
DOI : 10.1142/S021819590400141X

E. Lee, The rational Bézier representation for conics, Algorithms and New Trends. SIAM, pp.3-19, 1985.

J. Sánchez-reyes, Characteristics of conic segments in Bézier form, International Conference on Innovative Methods in Product Design, pp.231-234, 2011.

L. Garnier, L. Druoton, and R. Langevin, Subdivisions itératives d'arcs d'ellipses et d'hyperboles et applicationàapplicationà la visualisation de cyclides de Dupin, pp.1-36, 2012.

L. Garnier, L. Druoton, and J. P. Bécar, Points massiques, espace des sphères et " hyperbole, 2015.

K. J. Versprille, Computer-aided Design Applications of the Rational B-spline Approximation Form, p.7607690, 1975.

L. Piegl and W. Tiller, The NURBS book. Monographs in visual communication, 1995.

G. Farin, From conics to NURBS: A tutorial and survey, IEEE Computer Graphics and Applications, vol.12, issue.5, pp.78-86, 1992.
DOI : 10.1109/38.156017

L. Druoton, L. Garnier, and R. Langevin, Iterative construction of Dupin cyclide characteristic circles using non-stationary Iterated Function Systems (IFS), Computer-Aided Design, vol.45, issue.2
DOI : 10.1016/j.cad.2012.10.042

L. Garnier, J. P. Bécar, G. Morin, and L. Fuchs, Une application de l'espace des sphres : détermination des sphères de Dandelin, LIRIS, 2015.

J. C. Fiorot and P. Jeannin, Courbes splines rationnelles, applicationsàapplicationsà la CAO, Volume RMA, vol.24, 1992.

R. Goldman, On the algebraic and geometric foundations of computer graphics, ACM Transactions on Graphics, vol.21, issue.1, pp.52-86, 2002.
DOI : 10.1145/504789.504792

G. Farin, NURBS from Projective Geometry to Pratical Use, Ltd, 1999.

G. Albrecht, J. P. Bécar, G. E. Farin, and D. Hansford, On the approximation order of tangent estimators, Computer Aided Geometric Design, vol.25, issue.2, pp.80-95, 2008.
DOI : 10.1016/j.cagd.2007.05.005

L. Garnier and L. Druoton, Constructions, dans l'espace des sphères, de carreaux de cyclides de DupinàDupinà bords circulaires, pp.17-40, 2013.

T. Ida, H. Takahashi, M. Marin, F. Ghourabi, and A. Kasem, Computational Construction of a Maximum Equilateral Triangle Inscribed in an Origami, Mathematical Software -ICMS 2006, pp.361-372, 2006.
DOI : 10.1007/11832225_36

F. Haftmann, Haskell-style Type Classes with Isabelle/Isar, 2014.

C. Doran and A. Lasenby, Geometric Algebra for Physicists, 2003.
DOI : 10.1017/CBO9780511807497

L. Dorst, D. Fontijne, and S. Mann, Geometric algebra for computer science, ACM SIGACT News, vol.39, issue.4, 2007.
DOI : 10.1145/1466390.1466396

H. Huzita, Axiomatic Development of Origami Geometry, Proceedings of the First International Meeting of Origami Science and Technology, pp.143-158, 1989.

T. Ida, F. Ghourabi, and K. Takahashi, Formalizing polygonal knot origami, Journal of Symbolic Computation, vol.69, 2014.
DOI : 10.1016/j.jsc.2014.09.031

H. Abe, Trisecting an Angle by Origami, Sugaku Seminar, 1980.

T. Ida, A. Kasem, F. Ghourabi, and H. Takahashi, Morley???s theorem revisited: Origami construction and automated proof, Journal of Symbolic Computation, vol.46, issue.5, pp.571-583, 2011.
DOI : 10.1016/j.jsc.2010.10.007

R. J. Lang, A computational algorithm for origami design, Proceedings of the twelfth annual symposium on Computational geometry , SCG '96, pp.98-105, 1996.
DOI : 10.1145/237218.237249

J. C. Bowers and I. Streinu, Rigidity of Origami Universal Molecules Automated Deduction in Geometry, pp.120-142, 2013.

D. Wang, Clifford algebraic calculus for geometric reasoning, pp.115-140, 1997.
DOI : 10.1007/BFb0022723

F. `-evre, S. Wang, and D. , In: Combining algebraic computing and term-rewriting for geometry theorem proving, pp.145-156, 1998.

T. Ida, Huzita's Basic Origami Fold in Geometric Algebra, 2014 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp.11-13, 2014.
DOI : 10.1109/SYNASC.2014.9

M. Kondo, T. Matsuo, Y. Mizoguchi, and H. Ochiai, A mathematica module for conformal geometric algebra and origami folding, SCSS 2016: 7th International Symposium on Symbolic Computation in Software Science. Volume 39 of EPiC Series in Computing., EasyChair, pp.68-80, 2016.

L. Fuchs and L. Théry, A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry, pp.51-67, 2011.
DOI : 10.1007/978-3-7091-4368-1

URL : https://hal.archives-ouvertes.fr/hal-00657901

L. Fuchs and L. Théry, Implementing Geometric Algebra Products with Binary Trees, Advances in Applied Clifford Algebras, pp.589-611, 2014.
DOI : 10.1007/s00006-014-0447-3

URL : https://hal.archives-ouvertes.fr/hal-01095495

G. Aragcamarasa, G. Arag, /. Arag, J. J. 'on, /. Rogr et al., References 1. A. Bogomolny. Viviani's 3D Analogue from Interactive Mathematics Miscellany and Puzzles, 2008.

F. Botana, M. Hohenwarter, P. Jani?i´jani?i´c, Z. Kovács, I. Petrovi´cpetrovi´c et al., Automated Theorem Proving in GeoGebra: Current Achievements, Journal of Automated Reasoning, vol.74, issue.3, pp.39-59, 2015.
DOI : 10.1007/s10817-015-9326-4

K. Brown, Polynomials For Sums of Square Roots Downloaded from http, 2016.

S. Chou, Mechanical Geometry Theorem Proving, 1987.
DOI : 10.1007/978-94-009-4037-6

D. Cox, J. Little, and D. Shea, Ideals Varieties and Algorithms, 2007.

W. Decker, G. Greuel, G. Pfister, and H. Schönemann, Singular 4-0-2 ? A computer algebra system for polynomial computations, 2015.

Z. Kovács and B. Parisse, Giac and GeoGebra ??? Improved Gr??bner Basis Computations, Computer Algebra and Polynomials Lecture Notes in Computer Science, vol.8942, pp.126-138, 2015.
DOI : 10.1007/978-3-319-15081-9_7

D. Kapur, Using Gr??bner bases to reason about geometry problems, Journal of Symbolic Computation, vol.2, issue.4, pp.399-408, 1986.
DOI : 10.1016/S0747-7171(86)80007-4

Z. Kovács and C. Sólyom-gecse, GeoGebra Tools with Proof Capabilities, 2016.

B. Kutzler and S. Stifter, On the application of Buchberger's algorithm to automated geometry theorem proving, Journal of Symbolic Computation, vol.2, issue.4, pp.389-397, 1986.
DOI : 10.1016/S0747-7171(86)80006-2

I. Petrovi´cpetrovi´c and P. Jani?i´jani?i´c, Integration of OpenGeoProver with GeoGebra, 2012.

T. J. Muñiz, Cálculo simbólico y geométrico. Editorial Síntesis, 1998.

Z. Ye, S. Chou, and X. Gao, An Introduction to Java Geometry Expert, Automated Deduction in Geometry, pp.189-195, 2011.
DOI : 10.1007/978-3-642-21046-4_10

S. C. Chou, S. Chou, X. Gao, and J. Zhang, Mechanical geometry theorem proving, with a foreword by Larry Wos References 1, 1988.
DOI : 10.1007/978-94-009-4037-6

S. C. Chou, Mechanical geometry theorem proving, 1987.
DOI : 10.1007/978-94-009-4037-6

Y. Malitsky, A. Sabharwal, H. Samulowitz, and M. Sellmann, Non-Model-Based Algorithm Portfolios for SAT, Theory and Applications of Satisfiability Testing (SAT, 2011.
DOI : 10.1007/978-3-540-74970-7_41

M. Nikoli´cnikoli´c, F. Mari´cmari´c, and P. Jani?i´jani?i´c, Simple algorithm portfolio for sat, Artificial Intelligence Review, pp.1-9, 2012.

M. Hohenwarter, GeoGebra: Ein Softwaresystem für dynamische Geometrie und Algebra der Ebene, 2002.

P. Jani?i´jani?i´c, GCLC ??? A Tool for Constructive Euclidean Geometry and More Than That, Proceedings of International Congress of Mathematical Software, pp.58-73, 2006.
DOI : 10.1007/11832225_6

W. Wernick, Triangle Constructions with Three Located Points, Mathematics Magazine, vol.55, issue.4, pp.227-230, 1982.
DOI : 10.2307/2690164

V. Marinkovi´cmarinkovi´c, ArgoTriCS ? Automated Triangle Construction Solver, Journal of Experimental & Theoretical Artificial Intelligence, 2016.

V. Marinkovi´cmarinkovi´c and P. Jani?i´jani?i´c, Towards Understanding Triangle Construction Problems, Intelligent Computer Mathematics -CICM 2012, 2012.

V. Marinkovi´cmarinkovi´c, P. Jani?i´jani?i´c, and P. Schreck, Computer Theorem Proving for Verifiable Solving of Geometric Construction Problems, 10th International Workshop on Automated Deduction in Geometry, pp.72-93, 2014.
DOI : 10.1007/978-3-319-21362-0_5

F. Mari´cmari´c, I. Petrovi´cpetrovi´c, D. Petrovi´cpetrovi´c, and P. Jani?i´jani?i´c, Formalization and implementation of algebraic methods in geometry, Proceedings First Workshop on CTP Components for Educational Software of Electronic Proceedings in Theoretical Computer Science, pp.63-81, 2011.

T. Hastie, R. Tibshirani, and J. Friedman, The Elements of Statistical Learning, 2001.

K. P. Murphy, Machine Learning: A Probabilistic Perspective, 2012.

D. Krstajic, L. J. Buturovic, D. E. Leahy, and S. Thomas, Cross-validation pitfalls when selecting and assessing regression and classification models, Journal of Cheminformatics, vol.6, issue.1, pp.1-15, 2014.
DOI : 10.1111/biom.12041

C. R. Rao, Linear Statistical Inference and its Applications, 1973.
DOI : 10.1002/9780470316436

F. Botana, M. Hohenwarter, P. Jani?i´jani?i´c, Z. Kovács, I. Petrovi´cpetrovi´c et al., Automated Theorem Proving in GeoGebra: Current Achievements, Journal of Automated Reasoning, vol.74, issue.3, pp.39-59, 2015.
DOI : 10.1007/s10817-015-9326-4

O. Giering, Affine and Projective Generalization of Wallace Lines, J. Geometry and Graphics, vol.1, pp.119-133, 1997.

M. Guzmán, An Extension of the Wallace-Simson Theorem: Projecting in Arbitrary Directions, The American Mathematical Monthly, vol.106, issue.6, pp.574-580, 1999.
DOI : 10.2307/2589470

S. Holzer and O. Labs, Illustrating the classification of real cubic surfaces, Algebraic Geometry and Geometric Modeling, pp.119-134, 2006.
DOI : 10.1007/978-3-540-33275-6_8

R. Johnson, Advanced Euclidean Geometry, 1960.

P. Pech, On Simson?Wallace Theorem and Its Generalizations, J. Geometry and Graphics, vol.9, pp.141-153, 2005.

P. Pech, On a 3D Extension of the Simson?Wallace Theorem, J. Geometry and Graphics, vol.18, pp.205-215, 2014.

P. Pech, Extension of Simson???Wallace Theorem on Skew Quadrilaterals and Further Properties, LNAI, vol.9201, pp.108-118, 2015.
DOI : 10.1007/978-3-319-21362-0_7

R. Riesinger, On Wallace Loci from the Projective Point of View, J. Geometry and Graphics, vol.8, pp.201-213, 2004.

?. Roanes, E. M. Lozano, ?. Roanes, and M. Lozano, Automatic Determination of Geometric Loci, 3D-Extension of Simson?Steiner Theorem. LNAI, pp.157-173, 1930.

L. Schläfli, On the Distribution of Surfaces of the Third Order into Species, in Reference to the Absence or Presence of Singular Points, and the Reality of Their Lines, Philosophical Transactions of the Royal Society of London, vol.153, issue.0, pp.193-241, 1863.
DOI : 10.1098/rstl.1863.0010

D. Wang, Elimination Methods, 2001.
DOI : 10.1007/978-3-7091-6202-6

URL : https://hal.archives-ouvertes.fr/inria-00100616

D. Wang, Elimination Practice. Software Tools and Applications, 2004.
DOI : 10.1142/9781848161207

URL : https://hal.archives-ouvertes.fr/inria-00100630

=. {?} and ?. K. For, Select a geometric entity O l with type Line from F such that O l .level ? O.level for all O ? F where O is with type Line

F. {o and }. , Select a geometric entity O c with type Circle from F such that O c .level ? O.level for all O ? F where O is with type Circle

K. , ?. K. , K. , F. {o, and }. , Select a geometric entity O p with type Point from F such that O p .level > 0 and O p .level ? O.level for all O ? F where O is with type Point

X. Chen, D. Song, and D. Wang, Automated generation of geometric theorems from images of diagrams, Annals of Mathematics and Artificial Intelligence, vol.8, issue.1, pp.3-4333
DOI : 10.1007/s10472-014-9433-7

R. Datta, J. Li, and J. Wang, Content-based image retrieval approaches and trends of the new age, Multimedia Information Retrieval, 2005.

Y. Jiang, Z. Zhou, and M. U. Chowdhury, Image retrieval based on the combination of color and keyword, Proceedings of the International Conference on Computer Science, Software Engineering, Information Technology, e-Business and Applications International Society for Computers and Their Applications (ISCA), pp.450-453, 2003.

S. Oyama, T. Kokubo, and T. Ishida, Domain-specific web search with keyword spices, IEEE Transactions on Knowledge and Data Engineering, vol.16, issue.1, pp.17-27, 2004.
DOI : 10.1109/TKDE.2004.1264819

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.8288

D. Song, D. Wang, and X. Chen, Discovering Geometric Theorems from Scanned and Photographed Images of Diagrams, Lecture Notes in Computer Science 9201, pp.149-165
DOI : 10.1007/978-3-319-21362-0_10

R. Zanibbi and B. Yuan, Keyword and image-based retrieval of mathematical expressions, Document Recognition and Retrieval XVIII, 2011.
DOI : 10.1117/12.873312

M. De-berg, M. Van-kreveld, M. Overmars, and O. Schwarzkopf, OIn o1 -> OIn o2 -> PLCAconnect o1 o2. References 1, Definition PLCAconnected : Prop := forall(o1 o2 : object), 1997.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development -Coq'Art: The Calculus of Inductive Constructions, 1998.
URL : https://hal.archives-ouvertes.fr/hal-00344237

C. Brun, J. Dufourd, and N. Magaud, Designing and proving correct a convex hull algorithm with hypermaps in Coq, Computational Geometry, vol.45, issue.8, pp.45436-457, 2012.
DOI : 10.1016/j.comgeo.2010.06.006

URL : https://hal.archives-ouvertes.fr/hal-00955400

A. G. Cohn and J. Renz, Qualitative Spatial Reasoning Handbook of Knowledge Representation, Chapt 13, pp.551-596, 2007.

R. Dapoigny and P. Barlatier, A Coq-Based Axiomatization of Tarski???s Mereogeometry, 12th Conference on Spatial Information Theory (COSIT2015), pp.108-129, 2015.
DOI : 10.1007/978-3-319-23374-1_6

J. Dufourd, Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof, Theoretical Computer Science, vol.403, issue.2-3, pp.133-159, 2008.
DOI : 10.1016/j.tcs.2008.02.012

J. Dufourd, An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps, Journal of Automated Reasoning, vol.47, issue.5, pp.19-51, 2009.
DOI : 10.1007/s10817-009-9117-x

J. Dufourd and Y. Bertot, Formal Study of Plane Delaunay Triangulation, 1st International Conference on Interactive Theorem Proving (ITP2010), pp.211-226, 2010.
DOI : 10.1007/978-3-642-14052-5_16

URL : https://hal.archives-ouvertes.fr/inria-00504027

G. Gonthier, Formal Proof -The Four Color Theorem, Notices of the AMS, vol.55, issue.11, pp.1382-1393, 2008.

C. Kosniowski, A First Course in Algebraic Topology, 1980.
DOI : 10.1017/CBO9780511569296

S. Moriguchi, M. Goto, and K. Takahashi, Towards Verified Construction for Planar Class of a Qualitative Spatial Representation, 7th International Symposium on Symbolic Computation in Software Science (SCSS2016), EPiC Series in Computing, pp.117-129, 2016.

S. Moriguchi, M. Goto, and K. Takahashi, Formalization of IPLCA, 2016.

O. Stock, Spatial and Temporal Reasoning, 1997.
DOI : 10.1007/978-0-585-28322-7

K. Takahashi, T. Sumitomo, and I. Takeuti, On Embedding a Qualitative Representation in a Two-Dimensional Plane, Spatial Cognition & Computation, vol.8, issue.1-2, pp.4-26, 2008.
DOI : 10.1080/13875860801944887

K. Takahashi, M. Goto, and H. Miwa, Construction of a Planar PLCA Expression: A Qualitative Treatment of Spatial Data, Agents and Artificial Intelligence LNCS, vol.9494, pp.298-315, 2015.
DOI : 10.1007/978-3-319-27947-3_16

M. Yamamoto, S. Nishizaki, M. Hagiya, and Y. Toda, Formalization of planar graphs, Higher Order Logic Theorem Proving and Its Applications, pp.369-384, 2005.
DOI : 10.1007/3-540-60275-5_77