Towards an intelligent and dynamic geometry book. (English) Zbl 1425.97002

Summary: The pursuit of an Intelligent and Dynamic Geometry Book should involve the study of how currently developing methodologies and technologies of geometry knowledge representation, management, deduction and discovery can be incorporated effectively into future education. Just as Doron Zeilberger pointed out in [Plane geometry: an elementary textbook by Shalosh B. Ekhad XIV (circa 2050) downloaded from the future, http://sites.math.rutgers.edu/~zeilberg/PG/nis.html] a geometry book from the future would be a computer program, in which all the theorems can be automatically discovered (and of course proved) by computer and beautiful illustrations can be automatically generated and dynamically modified. Such a prospect motivates studies on how to represent and manage digitised geometric knowledge on computer. The geometry book of the future (the \(\mathcal{I}\)nt\(\mathcal{D}\)yn\(\mathcal{G}\)eo\(\mathcal{B}\)ook) should be adaptive, collaborative, visual and intelligent. Adaptive because the contents should adapt itself to the curricula and readers. It will allow collaborative work and its contents would be collaboratively formed using a knowledge base open to contributions. Statements and proofs should be en-lighted by dynamic geometry sketches and diagrams, and the correctness of the proofs should be ensured by computer checking. The book will be intelligent, the reader should be able to ask closed or open questions, and can also for proof hints. The book should also provide interactive exercises with automatic correction. Such a cloud platform, freely available in all standard computational platforms and devices, collaborative, adaptive to each and every user’s profiles, should bring together a whole new generation of mathematical tools with impact in all levels of education. To realise such a book, a network of experts must be built, increasing the connections between several research communities, such as: mathematical knowledge management; computer theorem proving and discovery; education, aggregating expertise in areas such as Proofs in a Learning Context; Interfaces and Searching; Tools Integration; Learning Environments in the Cloud. In this paper the author tries to make the case for such an endeavour.


97U50 Computer-assisted instruction, e-learning (aspects of mathematics education)
68T05 Learning and adaptive systems in artificial intelligence
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T30 Knowledge representation
97G10 Comprehensive works on geometry education
Full Text: DOI


[1] Aleven, V; Popescu, O; Koedinger, KR; Moore, JD (ed.); Redfield, CL (ed.); Johnson, WL (ed.), Towards tutorial dialog to support self-explanation: adding natural language understanding to a cognitive tutor, 246-255, (2001), Amsterdam
[2] Balacheff, N., Caferra, R., Cerulli, M., Gaudin, N., Maracci, M., Mariotti, M.A., Muller, J.P., Nicaud, J.F., Occello, M., Olivero, F., Peltier, N., Pesty, S., Soury-Lavergne, S., Sutherland, R., Trgalova, J., Webber, C.: Baghera assessment project, designing an hybrid and emergent educational society. Tech. Rep. 81, Laboratoire Leibniz-IMAG (2003)
[3] Bertot, Y; Guilhot, F; Pottier, L, Visualizing geometrical statements with geoview, Electron. Notes Theor. Comput. Sci., 103, 49-65, (2004)
[4] Bokhove, C., Jones, K., Charlton, P., Mavrikis, M., Geraniou, E.: Authoring your own creative, electronic book for mathematics: the mc-squared project (July 2014) (ICMT-2014). http://eprints.soton.ac.uk/367609/
[5] Botana, F; Hohenwarter, M; Janičić, P; Kovács, Z; Petrović, I; Recio, T; Weitzhofer, S, Automated theorem proving in geogebra: current achievements, J. Autom. Reason., 55, 39-59, (2015) · Zbl 1356.68181
[6] Botana, F., Quaresma, P. (eds.): Automated Deduction in Geometry: 10th International Workshop, ADG 2014, Coimbra, July 9-11, 2014, Revised Selected Papers. Lecture Notes in Computer Science, vol. 9201, pp. 119-128. Springer, Cham (2015)
[7] Boutry, P., Braun, G., Narboux, J.: From Tarski to descartes: formalization of the arithmetization of euclidean geometry. In: Davenport, J.H., Ghourabi, F. (eds.) SCSS 2016, the 7th International Symposium on Symbolic Computation in Software Science. EPiC Series in Computing, vol. 39, p. 15. EasyChair, Tokyo (March 2016). https://hal.archives-ouvertes.fr/hal-01282550 · Zbl 1394.68349
[8] Boutry, P., Narboux, J., Schreck, P., Braun, G.: Using small scale automation to improve both accessibility and readability of formal proofs in geometry. In: Botana, F., Quaresma, P. (eds.) Preliminary Proceedings of the 10th International Workshop on Automated Deduction in Geometry (ADG 2014), 9-11 July 2014, University of Coimbra, Portugal. CISUC Technical Reports, No. 2014/01, pp. 31-50. CISUC (2014) · Zbl 1131.68094
[9] Braun, G., Boutry, P., Narboux, J.: From Hilbert to Tarski. In: 11th International Workshop on Automated Deduction in Geometry. Proceedings of ADG 2016, p. 19. Strasbourg (Jun 2016). https://hal.inria.fr/hal-01332044
[10] Braun, G., Narboux, J.: From Tarski to Hilbert. In: Ida, T., Fleuriot, J. (eds.) Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 7993, pp. 89-109. Springer, Berlin (2013). doi:10.1007/978-3-642-40672-0_7 · Zbl 1397.03019
[11] Braun, G., Narboux, J.: A synthetic proof of Pappus’ theorem in Tarski’s geometry. J. Autom. Reason. 23 (Apr. 2016). https://hal.inria.fr/hal-01176508 · Zbl 1405.03034
[12] Chen, X; Li, W; Luo, J; Wang, D; Campbell, JA (ed.); Carette, J (ed.); Reis, GD (ed.); Sojka, P (ed.); Wenzel, M (ed.); Sorge, V (ed.), Open geometry textbook: a case study of knowledge acquisition via collective intelligence, No. 7362, 432-437, (2012), Berlin · Zbl 1360.68804
[13] Chen, X.: Electronic geometry textbook: a geometric textbook knowledge management system. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P., Rideau, L., Rioboo, R., Sexton, A. (eds.) Intelligent Computer Mathematics. pp. 278-292. No. 6167 in Lecture Notes in Computer Science. Springer, Berlin (2010)
[14] Chen, X, Representation and automated transformation of geometric statements, J. Syst. Sci. Complex., 27, 382-412, (2014) · Zbl 1314.68301
[15] Chen, X., Wang, D.: Management of geometric knowledge in textbooks. Data Knowl. Eng. 73, 43-57 (2012). http://www.sciencedirect.com/science/article/pii/S0169023X11001431
[16] Chou, S.: Proving and discovering geometry theorems using Wu’s method. Ph.D. Thesis, The University of Texas, Austin (1985) · Zbl 0629.68087
[17] Chou, S.C., Gao, X.S., Zhang, J.Z.: A collection of 110 geometry theorems and their machine produced proofs using full-angles. Tech. Rep. TR-94-4, Department of Computer Science, The Wichita State University (Nov. 1994)
[18] Chou, SC; Gao, XS; Zhang, JZ, Automated generation of readable proofs with geometric invariants, I. multiple and shortest proof generation, J. Autom. Reason., 17, 325-347, (1996) · Zbl 0865.68109
[19] Chou, SC; Gao, XS; Zhang, JZ, Automated generation of readable proofs with geometric invariants, II. theorem proving with full-angles, J. Autom. Reason., 17, 349-370, (1996) · Zbl 0865.68110
[20] Chrysafiadi, K., Virvou, M.: Student modeling approaches: a literature review for the last decade. Expert Syst. Appl. 40(11), 4715-4729 (2013). http://www.sciencedirect.com/science/article/pii/S095741741300122X
[21] Cobo, P; Fortuny, J; Puertas, E; Richard, P, Agentgeom: a multiagent system for pedagogical support in geometric proof problems, Int. J. Comput. Math. Learn., 12, 57-79, (2007)
[22] Cueli, M., González-Castro, P., Krawec, J., Núñez, J.C., González-Pienda, J.A.: Hipatia: a hypermedia learning environment in mathematics. An. Psicol. Ann. Psychol. 32(1), 98-105 (2015). http://revistas.um.es/analesps/article/view/analesps.32.1.185641
[23] Fuchs, L., Théry, L.: A formalization of Grassmann-Cayley algebra in COQ and its application to theorem proving in projective geometry. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) Automated Deduction in Geometry. Lecture Notes in Computer Science, vol. 6877, pp. 51-67. Springer, Berlin (2011). doi:10.1007/978-3-319-21362-0 · Zbl 1350.68233
[24] Gillies, R.M.: Structuring cooperative group work in classrooms. Int. J. Educ. Res. 39(1-2), 35-49 (2003). http://www.sciencedirect.com/science/article/pii/S0883035503000727 · Zbl 1314.68301
[25] Génevaux, J.D., Narboux, J., Schreck, P.: Formalization of Wu’s simple method in coq. In: Jouannaud, J.P., Shao, Z. (eds.) Certified Programs and Proofs, Lecture Notes in Computer Science, vol. 7086, pp. 71-86. Springer, Berlin (2011). doi:10.1007/978-3-642-25379-9_8 · Zbl 1350.68234
[26] Grégoire, B., Pottier, L., Théry, L.: Proof certificates for algebra and their application to automatic geometry theorem proving. In: International Workshop on Automated Deduction in Geometry, pp. 42-59. Springer (2008) · Zbl 1302.68242
[27] Haralambous, Y., Quaresma, P.: Querying geometric figures using a controlled language, ontological graphs and dependency lattices. In: S.W., et al. (ed.) CICM 2014. LNAI, vol. 8543, pp. 298-311. Springer (2014) · Zbl 1304.68170
[28] Ida, T., Kasem, A., Ghourabi, F., Takahashi, H.: Morley’s theorem revisited: origami construction and automated proof. J. Symb. Comput. 46(5), 571-583 (2011). http://www.sciencedirect.com/science/article/pii/S0747717110001768 · Zbl 1211.51011
[29] Janičić, P.: GCLC—a tool for constructive euclidean geometry and more than that. In: Iglesias, A., Takayama, N. (eds.) Mathematical Software—ICMS 2006, Lecture Notes in Computer Science, vol. 4151, pp. 58-73. Springer (2006) · Zbl 1230.51024
[30] Janičić, P; Narboux, J; Quaresma, P, The area method: a recapitulation, J. Autom. Reason., 48, 489-532, (2012) · Zbl 1242.68281
[31] Janičić, P., Quaresma, P.: System description: GCLCprover + GeoThms. In: Furbach, U., Shankar, N. (eds.) Automated Reasoning, Lecture Notes in Computer Science, vol. 4130, pp. 145-150. Springer (2006)
[32] Jiang, J; Zhang, J, A review and prospect of readable machine proofs for geometry theorems, J. Syst. Sci. Complex., 25, 802-820, (2012) · Zbl 1291.68351
[33] Kapur, D, Using Gröbner bases to reason about geometry problems, J. Symb. Comput., 2, 399-408, (1986) · Zbl 0629.68087
[34] Kortenkamp, U., Blessing, A.M., Dohrmann, C., Kreis, Y., Libbrecht, P., Mercat, C.: Interoperable interactive geometry for Europe—first technological and educational results and future challenges of the intergeo project. In: CERME 6 (2006)
[35] Kortenkamp, U., Dohrmann, C., Kreis, Y., Dording, C., Libbrecht, P., Mercat, C.: Using the intergeo platform for teaching and research. In: Proceedings of the 9th International Conference on Technology in Mathematics Teaching (ICTMT-9) (2009) · Zbl 1131.68094
[36] Kovács, Z.: The Relation Tool in GeoGebra 5, pp. 53-71. Springer International Publishing (2015). doi:10.1007/978-3-319-21362-0_4 · Zbl 1434.97015
[37] Li, H; Gao, XS (ed.); Wang, D (ed.), Clifford algebra approaches to mechanical geometry theorem proving, 205-299, (2000), San Diego
[38] Lin, F.L., Hsieh, F.J., Hanna, G., de Villiers, M. (eds.): Proceedings of the ICMI study 19 conference: proof and proving in mathematics education, vol. 1. The Department of Mathematics, National Taiwan Normal University (2009)
[39] Lin, F.L., Hsieh, F.J., Hanna, G., de Villiers, M. (eds.): Proceedings of the ICMI study 19 conference: proof and proving in mathematics education, vol. 2. The Department of Mathematics, National Taiwan Normal University (2009)
[40] Luengo, V.: Some didactical and epistemological considerations in the design of educational software: the Cabri-Euclide example. Int. J. Comput. Math. Learn. 10(1), 1-29 (2005). https://hal.archives-ouvertes.fr/hal-00961977
[41] Magaud, N., Narboux, J., Schreck, P.: Formalizing desargues’ theorem in coq using ranks. In: Shin, S.Y., Ossowski, S. (eds.) SAC, pp. 1110-1115. ACM (2009) · Zbl 1248.68449
[42] Marinković, V, Argotrics—automated triangle construction solver, J. Exp. Theor. Artif. Intell., 0, 1-25, (2016)
[43] Marinković, V., Janičić, P., Schreck, P.: Computer theorem proving for verifiable solving of geometric construction problems, pp. 72-93. Springer International Publishing (2015). doi:10.1007/978-3-319-21362-0_5 · Zbl 1434.03032
[44] Martins, C., Couto, P., Fernandes, M., Bastos, C., Lobo, C., Faria, L., Carrapatoso, E.: PCMAT—Mathematics Collaborative Learning Platform, pp. 93-100. Springer, Berlin (2011). doi:10.1007/978-3-642-19917-2_12
[45] Matsuda, N; Vanlehn, K, Gramy: a geometry theorem prover capable of construction, J. Autom. Reason., 32, 3-33, (2004)
[46] Matsuda, N., Van Lehn, K.: Advanced geometry tutor: an intelligent tutor that teaches proof-writing with construction. In: Artificial Intelligence in Education—Supporting Learning through Intelligent and Socially Informed Technology, Proceedings of the 12th International Conference on Artificial Intelligence in Education, AIED 2005, pp. 443-450, Amsterdam (18-22 July 2005) · Zbl 0865.68110
[47] Mendicino, M; Razzaq, L; Heffernan, NT, A comparison of traditional homework to computer-supported homework, J. Res. Technol. Educ., 41, 331-359, (2009)
[48] Monaghan, J., Trouche, L., Borwein, J.: Tools and Mathematics. Springer International Publishing, Berlin (2016)
[49] Moraes, T.G., Santoro, F.M., Borges, M.R.: Tabulæ: educational groupware for learning geometry. In: 5th IEEE International Conference on Advanced Learning Technologies, 2005. ICALT 2005, pp. 750-754 (July 2005) · Zbl 1291.68351
[50] Moriyón, R., Saiz, F., Mora, M.: GeoThink: An Environment for Guided Collaborative Learning of Geometry, Nuevas Ideas en Informática Educativa, vol. 4, pp. 200-2008. J. Sánchez (ed), Santiago de Chile (2008)
[51] Narboux, J.: A decision procedure for geometry in coq. In: Slind Konrad, Bunker Annette, G.G.C. (ed.) Theorem Proving in Higher Order Logics 2004. vol. 3223, pp. 225-240. Springer, Park City (Jul 2004). https://hal.inria.fr/inria-00001035 · Zbl 1099.68734
[52] Narboux, J.: Mechanical theorem proving in Tarski’s geometry. In: Eugenio Roanes Lozano, F.B. (ed.) Automated Deduction in Geometry 2006. vol. 4869, pp. 139-156. Francisco Botana, Springer, Pontevedra (Aug 2006). https://hal.inria.fr/inria-00118812 · Zbl 1195.03019
[53] Narboux, J, A graphical user interface for formal proofs in geometry, J. Autom. Reason., 39, 161-180, (2007) · Zbl 1131.68094
[54] Narboux, J.: Mechanical theorem proving in Tarski’s geometry. In: Proceedings of Automatic Deduction in Geometry 06. Lecture Notes in Artificial Intelligence, vol. 4869, pp. 139-156. Springer (2007) · Zbl 1195.03019
[55] Quaresma, P., Janičić, P., Tomašević, J., Vujošević-Janičić, M., Tošić, D.: Communicating Mathematics in The Digital Era, chap. XML-Bases Format for Descriptions of Geometric Constructions and Proofs, pp. 183-197. A. K. Peters, Ltd. (2008)
[56] Quaresma, P.: Thousands of geometric problems for geometric theorem provers (TGTP). In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 6877, pp. 169-181. Springer (2011) · Zbl 1350.68243
[57] Quaresma, P., Baeta, N.: Current status of the I2GATP common format. In: Botana, F., Quaresma, P. (eds.) Automated Deduction in Geometry: 10th International Workshop, ADG 2014, Coimbra, July 9-11, 2014, Revised Selected Papers. Lecture Notes in Computer Science, vol. 9201, pp. 119-128. Springer, Cham (2015) · Zbl 1434.68643
[58] Quaresma, P., Santos, V., Bouallegue, S.: The Web Geometry Laboratory project. In: CICM 2013. LNAI, vol. 7961, pp. 364-368. Springer (2013) · Zbl 1390.97006
[59] Richard, P; Fortuny, J, Amélioration des compétences argumentatives à l’aide d’un systéme tutoriel en classe de mathématique au secondaire, Ann. didact. Sci. Cognit., 12, 83-116, (2007)
[60] Richard, P., Fortuny, J., Hohenwarter, M., Gagnon, M.: GeogebraTUTOR: une nouvelle approche pour la recherche sur l’apprentissage compétentiel et instrumenté de la géométrie à l’école secondaire. In: Bastiaens, T., Carliner, S. (eds.) Proceedings of E-Learn: World Conference on E-Learning in Corporate, Government, Healthcare, and Higher Education 2007. No. 428-435, Association for the Advancement of Computing in Education (AACE), Chesapeake (2007)
[61] Richter-Gebert, J., Kortenkamp, U.: The Interactive Geometry Software Cinderella. Springer, Berlin (1999) · Zbl 0926.51002
[62] Santiago, E., Hendriks, M., Kreis, Y., Kortenkamp, U., Marquès, D.: i2g Common file format final version. Tech. Rep. D3.10, The Intergeo Consortium (2010). http://i2geo.net/xwiki/bin/view/I2GFormat/ · Zbl 1356.68181
[63] Santos, V., Quaresma, P., Campos, H., Marić, M.: Web Geometry Laboratory: case studies in Portugal and Serbia. In: Interactive Learning Environments, pp. 1-19 (Dec 2016) (online). doi:10.1080/10494820.2016.1258715 · Zbl 0855.68086
[64] Shute, V., Psotka, J.: The handbook of research for educational communications and technology, chap. In: Intelligent Tutoring Systems: Past, Present, and Future, 1st edn, pp. 570-600. The Association for Educational Communications and Technology (2001)
[65] Sinclair, N; Bartolini Bussi, MG; Villiers, M; Jones, K; Kortenkamp, U; Leung, A; Owens, K, Recent research on geometry education: an ICME-13 survey team report, ZDM Math. Educ., 48, 691-719, (2016)
[66] Stojanović, S., Narboux, J., Bezem, M., Janičić, P.: A vernacular for coherent logic. In: Watt, S., Davenport, J., Sexton, A., Sojka, P., Urban, J. (eds.) Intelligent Computer Mathematics, Lecture Notes in Computer Science, vol. 8543, pp. 388-403. Springer International Publishing (2014). doi:10.1007/978-3-319-08434-3_28 · Zbl 1304.68163
[67] Stojanovic, S., Pavlovic, V., Janicic, P.: A coherent logic based geometry theorem prover capable of producing formal and readable proofs. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) Automated Deduction in Geometry, pp. 201-220. Springer, Berlin, Heidelberg (2010) · Zbl 1252.68264
[68] Summers, J; Beretvas, S; Svinicki, M; Gorin, J, Evaluating collaborative learning and community, J. Exp. Educ., 73, 165-188, (2005)
[69] Triantafillou, E., Pomportsis, A., Demetriadis, S.: The design and the formative evaluation of an adaptive educational system based on cognitive styles. Comput. Educ. 41(1), 87-103 (2003). http://www.sciencedirect.com/science/article/pii/S0360131503000319
[70] Wang, D; Pfalzgraf, J (ed.); Wang, D (ed.), Reasoning about geometric problems using an elimination method, 147-185, (1995), New York · Zbl 0855.68086
[71] Wang, D., Chen, X., An, W., Jiang, L., Song, D.: Opengeo: an open geometric knowledge base. In: Hong, H., Yap, C. (eds.) Mathematical Software—ICMS 2014, Lecture Notes in Computer Science, vol. 8592, pp. 240-245. Springer, Berlin (2014). doi:10.1007/978-3-662-44199-2_38 · Zbl 1434.68665
[72] Wang, K., Su, Z.: Automated geometry theorem proving for human-readable proofs. In: Proceedings of the 24th International Conference on Artificial Intelligence, pp. 1193-1199. IJCAI’15, AAAI Press (2015). http://dl.acm.org/citation.cfm?id=2832249.2832414 · Zbl 1242.68281
[73] Wu, W.: Automated Theorem Proving: After 25 Years, vol. 29, chap. On the Decision Problem and the Mechanization of Theorem Proving in Elementary Geometry, pp. 213-234. American Mathematical Society (1984)
[74] Ye, Z., Chou, S.C., Gao, X.S.: An introduction to java geometry expert. In: Sturm, T., Zengler, C. (eds.) Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 6301, pp. 189-195. Springer, Berlin (2011). doi:10.1007/978-3-642-21046-4_10, jGEX · Zbl 1302.68247
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.