Automated deduction and knowledge management in geometry. (English) Zbl 1474.68453

Summary: Scientific research and education at all levels are concerned primarily with the discovery, verification, communication, and application of scientific knowledge. Learning, reusing, inventing, and archiving are the four essential aspects of knowledge accumulation in mankind’s civilisation process. In this cycle of knowledge accumulation, which has been supported for thousands of years by written books and other physical means, rigorous reasoning has always played an essential role. Nowadays this process is becoming more and more effective due to the availability of new paradigms based on computer applications. Geometric reasoning with such computer applications is one of the most attractive challenges for future accumulation and dissemination of knowledge.


68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
51-08 Computational methods for problems pertaining to geometry
68V30 Mathematical knowledge management
Full Text: DOI


[1] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development (Coq’Art: The Calculus of Inductive Constructions). Springer, EATCS (2004) · Zbl 1069.68095
[2] Botana, F., Hohenwarter, M., Janičić, P., Kovács, Z., Petrović, Ivan, R., Tomás, W.S.: Automated theorem proving in GeoGebra: current achievements. J. Autom. Reason. 55(1), 39-59 (2015) · Zbl 1356.68181
[3] Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems: 25 Years of TACAS: TOOLympics, Volume 11429 of LNCS. Springer, 2019. Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11 (2019) · Zbl 1408.68008
[4] Botana, F.; Kovács, Z.; Recio, T.; Fleuriot, J.; Wang, D.; Calmet, J., Towards an automated geometer, Artificial Intelligence and Symbolic Computation, 215-220 (2018), Cham: Springer, Cham
[5] Botana, F.; Valcarce, JL, A dynamic-symbolic interface for geometric theorem discovery, Comput. Educ., 38, 21-35 (2002)
[6] Baeta, N., Quaresma, P.: The full angle method on the OpenGeoProver. In: Lange, C., Aspinall, D., Carette, J., Davenport, J., Kohlhase, A., Kohlhase, M., Libbrecht, P., Quaresma, P., Rabe, F., Sojka, P., Whiteside, I., Windsteiger, W. (eds.) MathUI, OpenMath, PLMMS and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, number 1010 in CEUR Workshop Proceedings, Aachen (2013)
[7] Baeta, N., Quaresma, P.: Towards ranking geometric automated theorem provers. In: Quaresma, P., Neuper, W. (eds.) Proceedings 7th International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18 July 2018, volume 290 of Electronic Proceedings in Theoretical Computer Science, pp. 30-37. Open Publishing Association (2019)
[8] Baeta, N., Quaresma, P., Kovács, Z.: Towards a geometry automated provers competition. In: Proceedings 8th International Workshop on Theorem proving Components for Educational Software, Volume 313 of Electronic Proceedings in Theoretical Computer Science, pp. 93-100, February 2020. (ThEdu’19), Natal, Brazil, 25th August (2019)
[9] Budd Rowe, M.: Wait-time and rewards as instructional variables: Their influence on language, logic, and fate control. Technical report, National Association for Research in Science Teaching (1972)
[10] Budd Rowe, M., Wait time: slowing down may be a way of speeding up!, J. Teach. Educ., 37, 1, 43-50 (1986)
[11] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C., All About Maude—A High-Performance Logical Framework (Pb). Lecture Notes in Computer Science (2007), New York: Springer, New York · Zbl 1115.68046
[12] Chou, S-C; Gao, X-S; Robinson, JA; Voronkov, A., Automated reasoning in geometry, Handbook of Automated Reasoning, 707-749 (2001), Amsterdam: Elsevier, Amsterdam · Zbl 1011.68128
[13] Chou, S-C; Gao, X-S; Zhang, J-Z, Machine Proofs in Geometry (1994), Singapore: World Scientific, Singapore
[14] Chou, S-C; Gao, X-S; Zhang, J-Z, Automated generation of readable proofs with geometric invariants, I. Multiple and shortest proof generation, J. Autom. Reason., 17, 13, 325-347 (1996) · Zbl 0865.68109
[15] Chou, S-C; Gao, X-S; Zhang, J-Z, Automated generation of readable proofs with geometric invariants, II. Theorem proving with full-angles, J. Autom. Reason., 17, 13, 349-370 (1996) · Zbl 0865.68110
[16] Chen, X., Electronic geometry textbook: a geometric textbook knowledge management system, Intelligent Computer Mathematics. Number 6167 in LNCS, 278-292 (2010), Berlin: Springer, Berlin · Zbl 1286.68425
[17] Chen, X., Representation and automated transformation of geometric statements, J. Syst. Sci. Complex., 27, 2, 382-412 (2014) · Zbl 1314.68301
[18] Chou, S.C.: Proving and discovering geometry theorems using Wu’s method. Ph.D. thesis, The University of Texas, Austin (1985)
[19] Chou, S-C, Mechanical Geometry Theorem Proving (1987), Dordrecht: D. Reidel Publishing Company, Dordrecht
[20] Chen, X.; Li, W.; Luo, J.; Wang, D.; Autexier, S.; Campbell, J.; Rubio, J.; Sorge, V.; Suzuki, M.; Wiedijk, F., Open geometry textbook: a case study of knowledge acquisition via collective intelligence, Intelligent Computer Mathematics, 432-437 (2012), Berlin: Springer, Berlin · Zbl 1360.68804
[21] Chein, M.; Mugnier, M-L, Graph-Based Knowledge Representation: Computational Foundations of Conceptual Graphs. Advanced Information and Knowledge Processing Series (2009), New York: Springer, New York · Zbl 1168.68043
[22] Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) Automata Theory and Formal Languages 2nd GI Conference Kaiserslautern, May 20-23, 1975. Lecture Notes in Computer Science, vol. 33. Springer, Berlin (1975) · Zbl 0318.02051
[23] Coelho, H.; Pereira, LM, Automated reasoning in geometry theorem proving with Prolog, J. Autom. Reason., 2, 4, 329-390 (1986) · Zbl 0642.68161
[24] Chen, X.; Wang, D., Management of geometric knowledge in textbooks, Data Knowl. Eng., 73, 43-57 (2012)
[25] de Bruijn, NG, A survey of the project Automath, Selected Papers on Automath. Volume 133 of Studies in Logic and the Foundations of Mathematics, 41-161 (1994), Amsterdam: North-Holland, Amsterdam
[26] Dhar, S., Roy, S., Das, S.: A Critical Survey of Mathematical Search Engines. In: Computational Intelligence, Communications, and Business Analytics, pp. 193-207. Springer, New York (2019)
[27] Font, L., Richard, P.R., Gagnon, M.: Improving qed-tutrix by automating the generation of proofs. In: Quaresma, P., Neuper, W. (eds.) Proceedings 6th International Workshop on Theorem Proving Components for Educational Software, Gothenburg, Sweden, 6 Aug 2017, volume 267 of Electronic Proceedings in Theoretical Computer Science, pp. 38-58. Open Publishing Association (2018)
[28] Gelernter, H.: Realization of a geometry-theorem proving machine. In: Computers & Thought, 2nd edn., pp. 134-152. MIT Press, Cambridge (1995)
[29] Gelernter, H., Hansen, J.R., Loveland, D.W.: Empirical explorations of the geometry theorem machine. In: Papers Presented at the May 3-5, 1960, Western Joint IRE-AIEE-ACM Computer Conference, IRE-AIEE-ACM ’60 (Western), pp. 143-149. ACM, New York (1960)
[30] Gagnon, M., Leduc, N., Richard, P.R., Tessier-Baillargeon, M.: Qed-tutrix: creating and expanding a problem database towards personalized problem itineraries for proof learning in geometry. In: Proceedings of the Tenth Congress of the European Society for Research in Mathematics Education (CERME10) (2017)
[31] Hanna, G., Proof, explanation and exploration: an overview, Educ. Stud. Math., 44, 1-2, 5-23 (2000)
[32] Hearst, MA, Search User Interfaces (2009), Cambridge: Cambridge University Press, Cambridge
[33] Han, T.A., Pereira, L.M., Lenaerts, T.: Modelling and influencing the AI bidding war: a research agenda. In: AAAI/ACM Conference on AI, Ethics and Society 2019, vol. 1 (2019)
[34] Haralambous, Y.; Quaresma, P.; Watt, S., Querying geometric figures using a controlled language, ontological graphs and dependency lattices, CICM 2014, Volume 8543 of LNAI, 298-311 (2014), New York: Springer, New York · Zbl 1304.68170
[35] Haralambous, Y., Quaresma, P.: Geometric search in TGTP. In: Li, H. (ed.) Proceedings of the 12th International Conference on Automated Deduction in Geometry. SMS International (2018) · Zbl 1304.68170
[36] Hanna, G.; Reid, D.; de Villiers, M., Proof Technology in Mathematics Research and Teaching (2019), New York: Springer, New York · Zbl 1451.97008
[37] Janičić, P.; Iglesias, A.; Takayama, N., GCLC—a tool for constructive euclidean geometry and more than that, Mathematical Software—ICMS 2006, Volume 4151 of Lecture Notes in Computer Science, 58-73 (2006), New York: Springer, New York · Zbl 1230.51024
[38] Janičić, P.; Narboux, J.; Quaresma, P., The Area method: a recapitulation, J. Autom. Reason., 48, 4, 489-532 (2012) · Zbl 1242.68281
[39] Janičić, P.; Quaresma, P.; Furbach, U.; Shankar, N., System description: GCLCprover + GeoThms, Automated Reasoning, Volume 4130 of Lecture Notes in Computer Science, 145-150 (2006), New York: Springer, New York
[40] Janičić, P.; Quaresma, P.; Botana, F.; Recio, T., Automatic verification of regular constructions in dynamic geometry systems, Automated Deduction in Geometry, Volume 4869 of Lecture Notes in Computer Science, 39-51 (2007), New York: Springer, New York · Zbl 1195.68092
[41] Kapur, D.: Geometry theorem proving using Hilbert’s nullstellensatz. In: SYMSAC ’86: Proceedings of the fifth ACM symposium on Symbolic and algebraic computation, pp. 202-208. ACM Press, New York (1986)
[42] Kapur, D., Using Gröbner bases to reason about geometry problems, J. Symb. Comput., 2, 4, 399-408 (1986) · Zbl 0629.68087
[43] 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)
[44] Kovács, Z.; Botana, F.; Quaresma, P., The relation tool in geogebra 5, Automated Deduction in Geometry, 53-71 (2015), New York: Springer, New York · Zbl 1434.97015
[45] Leduc, N.: QED-Tutrix : système tutoriel intelligent pour l’accompagnement d’élèves en situation de résolution de problèmes de démonstration en géométrie plane. Ph.D. thesis, École polytechnique de Montréal (2016)
[46] Lemoine, É.: Géométrographie ou Art des constructions géométriques, volume 18 of Phys-Mathématique. Scentia, Sydney (1902) · JFM 33.0510.02
[47] Li, H.; Gao, X-S; Wang, D., Clifford algebra approaches to mechanical geometry theorem proving, Mathematics Mechanization and Applications, 205-299 (2000), San Diego: Academic Press, San Diego
[48] Mackay, JS, The geometrography of euclid’s problems, Proc. Edinb. Math. Soc., 12, 2-16 (1893) · JFM 25.0900.09
[49] Meseguer, J.; Ölveczky, PC, Twenty years of rewriting logic, Rewriting Logic and Its Applications, 15-17 (2010), Berlin: Springer, Berlin · Zbl 1306.68082
[50] Kovács, Z.; Nikolić, P.; Mladen, J.; Marinković, V., Portfolio theorem proving and prover runtime prediction for geometry, Ann. Math. Artif. Intell., 85, 119-146 (2019) · Zbl 1431.68123
[51] Moraes, T.G., Santoro, F.M., Borges, M.R.S.: Tabulæ: educational groupware for learning geometry. In: Fifth IEEE International Conference on Advanced Learning Technologies, 2005. ICALT 2005, pp. 750-754 (2005)
[52] Moriyón, R., Saiz, F., Mora, M.: GeoThink: An Environment for Guided Collaborative Learning of Geometry, volume 4 of Nuevas Ideas en Informática Educativa, pp. 200-2008. J. Sánchez (ed.), Santiago de Chile (2008)
[53] Mathis, P.; Thierry, SEB, A formalization of geometric constraint systems and their decomposition, Formal Asp. Comput., 22, 2, 129-151 (2010) · Zbl 1214.68437
[54] Narboux, J., A graphical user interface for formal proofs in geometry, J. Autom. Reason., 39, 161-180 (2007) · Zbl 1131.68094
[55] Pambuccian, V., The simplest axiom system for plane hyperbolic geometry, Stud. Log., 77, 3, 385-411 (2004) · Zbl 1069.03007
[56] Pinheiro, VA, Geometrografia 1 (1974), Rio de Janeiro: Bahiense, Rio de Janeiro
[57] Petrović, I., Kovács, Z., Weitzhofer, S., Hohenwarter, M., Janičić, P.: Extending GeoGebra with automated theorem proving by using OpenGeoProver. In: Proceedings CADGME 2012, Novi Sad, Serbia (2012) · Zbl 1356.68181
[58] Quaresma, P., Baeta, N.: Geometry automated theorem provers systems competition 0.2 report. Techreport 1, CISUC (2019)
[59] Quaresma, P., Nuno, B.: Current status of the I2GATP common format. In: Botana, F., Quaresma, P. (eds.) Proceedings ADG 2014, Volume 2014 of CISUC Technical Report, pp. 67-74. CISUC (2014) · Zbl 1434.68643
[60] Quaresma, P.; Santos, V.; Hanna, G.; Reid, DA; de Villiers, M., Computer-generated geometry proofs in a learning context, Proof Technology in Mathematics Research and Teaching (2019), New York: Springer, New York
[61] Quaresma, P.; Santos, V.; Graziani, P.; Baeta, N., Taxonomy of geometric problems, J. Symb. Comput., 97, 31-55 (2020) · Zbl 1444.68292
[62] Quaresma, P.; Santos, V.; Marić, M., WGL, a web laboratory for geometry, Educ. Inf. Technol., 23, 1, 237-252 (2018)
[63] Quaife, A., Automated development of Tarski’s geometry, J. Autom. Reason., 5, 97-118 (1989) · Zbl 0683.68082
[64] Quaresma, P.; Schreck, P.; Narboux, J.; Richter-Gebert, J., Thousands of geometric problems for geometric Theorem Provers (TGTP), Automated Deduction in Geometry, volume 6877 of Lecture Notes in Computer Science, 169-181 (2011), New York: Springer, New York · Zbl 1350.68243
[65] Quaresma, P.; Fleuriot, J.; Wang, D.; Calmet, J., Automatic deduction in an AI geometry book, Artificial Intelligence and Symbolic Computation, volume 11110 of Lecture Notes in Computer Science, 221-226 (2018), New York: Springer, New York
[66] Richter-Gebert, J.; Kortenkamp, U., The Interactive Geometry Software Cinderella (1999), New York: Springer, New York · Zbl 0926.51002
[67] Recio, T.; Vélez, MP, Automatic discovery of theorems in elementary geometry, J. Autom. Reason., 23, 63-82 (1999) · Zbl 0941.03010
[68] Santos, V.; Baeta, N.; Quaresma, P., Geometrography in dynamic geometry, Int. J. Technol. Math. Educ., 26, 2, 89-96 (2019)
[69] Santiago, E., Hendriks, M., Kreis, Y., Kortenkamp, U., Marquès, D.: i2g Common File Format Final Version. Technical report D3.10, The Intergeo Consortium (2010)
[70] Stojanović, S.; Pavlović, V.; Janičić, P.; Schreck, P.; Narboux, J.; Richter-Gebert, J., A coherent logic based geometry theorem prover capable of producing formal and readable proofs, Automated Deduction in Geometry, Volume 6877 of Lecture Notes in Computer Science, 201-220 (2011), Berlin: Springer, Berlin · Zbl 1252.68264
[71] Stahl, R.J.: Using “think-time” and “wait-time” skillfully in the classroom. Technical report, ERIC Digest (1994)
[72] Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483-502 (2017) · Zbl 1425.68381
[73] Tarski, A.: A decision method for elementary algebra and geometry. Technical report, RAND Corporation (1951) · Zbl 0044.25102
[74] van Dalen, D.: Logic and Structure. Universitext, Springer (1980) · Zbl 0434.03001
[75] Wang, D.; Pfalzgraf, J.; Wang, D., Reasoning about geometric problems using an elimination method, Automated Pratical Reasoning, 147-185 (1995), New York: Springer, New York · Zbl 0855.68086
[76] Wang, D.; Chen, X.; An, W.; Jiang, L.; Song, D.; Hong, H.; Yap, C., Opengeo: an open geometric knowledge base, Mathematical Software—ICMS 2014, volume 8592 of Lecture Notes in Computer Science, 240-245 (2014), Berlin: Springer, Berlin · Zbl 1434.68665
[77] Wiedijk, F.: The de Bruijn factor. Poster at International Conference on Theorem Proving in Higher Order Logics (TPHOL2000), 2000. Portland, Oregon, USA, 14-18 August (2000)
[78] Wu, W.-T.: On the decision problem and the mechanization of theorem proving in elementary geometry. In: Automated Theorem Proving: After 25 Years, Volume 29 of Contemporary Mathematics, pp. 213-234. American Mathematical Society (1984)
[79] Wong, W-K; Yin, S-K; Yang, H-H; Cheng, Y-H, Using computer-assisted multiple representations in learning geometry proofs, Educ. Technol. Soc., 14, 3, 43-54 (2011)
[80] Ye, Z.; Chou, S-C; Gao, X-S, Visually dynamic presentation of proofs in plane geometry, part 1, J. Autom. Reason., 45, 213-241 (2010) · Zbl 1211.68372
[81] Ye, Z.; Chou, S-C; Gao, X-S; Sturm, T.; Zengler, C., An introduction to Java geometry expert, Automated Deduction in Geometry, Volume 6301 of Lecture Notes in Computer Science, 189-195 (2011), Berlin: Springer, Berlin
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.