×

Taxonomies of geometric problems. (English) Zbl 1444.68292

Summary: In the current Information Society the organisation of the information is key to ensure the information safekeeping and retrieval. It is of utmost importance that each and every user can find the information he/she is looking for, presented in such a way that best fit his/her needs. Geometry is no exception, the servers of geometric information should be easily and successfully searchable. By classifying the information contained in the servers of geometric information accordingly to several taxonomies, it will be possible to begin applying filters to the users’ queries, adjusting them to the perceived user’s needs. Having that in mind, the introduction of an adaptive filtering mechanisms into servers of geometric information is considered.
Different taxonomies for different goals are presented. For educational purposes, a classification like Common Core Standards should be considered, but other considerations like the complexity of the construction, the provability, by a geometry automatic theorem prover, of a given conjecture and the readability of the resulting proof, should be taken into account. For research in automated deduction purposes, other issues must be considered, e.g. efficiency and applicability of the available automated provers. To validate the usefulness of these taxonomies it will be used, as a case study, their application to a server of geometric information. In particular, Thousands of Geometric problems for geometric Theorem Provers will be considered. TGTP is a Web-based repository of geometric problems being developed to support the testing and evaluation of geometric automated theorem proving systems. Using this system it will be analysed how the taxonomies could help to tailor the search for information adapted to each and every geometer.

MSC:

68V30 Mathematical knowledge management
68U05 Computer graphics; computational geometry (digital and algorithmic aspects)
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68V35 Digital mathematics libraries and repositories
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Altshiller-Court, Nathan, College Geometry: An Introduction to the Modern Geometry of the Triangle and the Circle (Dover Books on Mathematics) (2007), Dover Publications, unabridged republication of the second edition of the work · Zbl 1208.51001
[2] Botana, Francisco; Hohenwarter, Markus; Janičić, Predrag; Kovács, Zoltán; Petrović, Ivan; Recio, Tomás; Weitzhofer, Simon, Automated theorem proving in GeoGebra: current achievements, J. Autom. Reason., 55, 1, 39-59 (2015) · Zbl 1356.68181
[3] Boutry, Pierre; Narboux, Julien; Schreck, Pascal; Braun, Gabriel, Using small scale automation to improve both accessibility and readability of formal proofs in geometry, (Botana, Francisco; Quaresma, Pedro, Preliminary Proceedings of the 10th International Workshop on Automated Deduction in Geometry. Preliminary Proceedings of the 10th International Workshop on Automated Deduction in Geometry, ADG 2014 (2014)), 31-49, number 2014/001 in CISUC Technical Reports, Coimbra, Portugal, CISUC
[4] Chou, Shang-Ching, Mechanical Geometry Theorem Proving (1988), D. Reidel Publishing Company · Zbl 0661.14037
[5] Chou, Shang-Ching; Gao, Xiao-Shan, Automated reasoning in geometry, (Robinson, John Alan; Voronkov, Andrei, Handbook of Automated Reasoning (2001), Elsevier Science Publishers B.V.), 707-749 · Zbl 1011.68128
[6] Chou, Shang-Ching; Gao, Xiao-Shan; Zhang, Jing-Zhong, Machine Proofs in Geometry (1994), World Scientific · Zbl 0941.68503
[7] Chou, Shang-Ching; Gao, Xiao-Shan; Zhang, Jing-Zhong, Automated generation of readable proofs with geometric invariants, I. Multiple and shortest proof generation, J. Autom. Reason., 17, 3, 325-347 (1996) · Zbl 0865.68109
[8] Chou, Shang-Ching; Gao, Xiao-Shan; Zhang, Jing-Zhong, Automated generation of readable proofs with geometric invariants, II. Theorem proving with full-angles, J. Autom. Reason., 17, 3, 349-370 (1996) · Zbl 0865.68110
[9] Chou, Shang-Ching; Gao, Xiao-Shan; Zhang, Jing-Zhong, A deductive database approach to automated geometry theorem proving and discovering, J. Autom. Reason., 25, 3, 219-246 (2000) · Zbl 0961.68121
[10] Coelho, Helder; Pereira, Luis Moniz, Automated reasoning in geometry theorem proving with Prolog, J. Autom. Reason., 2, 4, 329-390 (December 1986)
[11] de Bruijn, Nicolaas Govert, Selected papers on automath, (A survey of the project Automath. A survey of the project Automath, Studies in Logic and the Foundations of Mathematics, vol. 133 (1994), Elsevier: Elsevier Amsterdam), 141-161
[12] de Villiers, Michael, The role and function of proof in mathematics, Pythagoras, 24, 17-24 (1990)
[13] Gelernter, Herbert, Realization of a geometry-theorem proving machine, (Computers & Thought (1995), MIT Press: MIT Press Cambridge, MA, USA), 134-152
[14] Grüttner, Adalbert, Die Grundlagen der Geometrographie (1912), Nischkowsky: Nischkowsky Breslau · JFM 43.0579.02
[15] Hanna, Gila, Proof, explanation and exploration: an overview, Educ. Stud. Math., 44, 1-2, 5-23 (2000)
[16] (Hanna, Gila; de Villiers, Michael, Proof and Proving in Mathematics Education. Proof and Proving in Mathematics Education, New ICMI Study Series, vol. 15 (2012), Springer) · Zbl 1234.00015
[17] Hanna, Gila; Sidoli, Nathan, Visualisation and proof: a brief survey of philosophical perspectives, ZDM, Zent.bl. Didakt. Math., 39, 1-2, 73-78 (2007)
[18] Haralambous, Yannis; Quaresma, Pedro, Querying geometric figures using a controlled language, ontological graphs and dependency lattices, (Watt, S. M.; Davenport, J. H.; Sexton, A. P.; Sojka, P.; Urban, J., CICM 2014. CICM 2014, LNAI, vol. 8543 (2014), Springer), 298-311 · Zbl 1304.68170
[19] Haralambous, Yannis; Quaresma, Pedro, Geometric search in TGTP, (Li, Hongbo, Proceedings of the 12th International Conference on Automated Deduction in Geometry (2018)), 19-25
[20] Hartshorne, Robin, Geometry: Euclid and Beyond (2000), Springer · Zbl 0954.51001
[21] Hearst, Marti A., Search User Interfaces (2009), Cambridge University Press
[22] Heath, Thomas L., The Thirteen Books of Euclid’s Elements, 3 vols (1908), Cambridge University Press
[23] Hohenwarter, Markus, Geogebra – a Software System for Dynamic Geometry and Algebra in the Plane (2002), University of Salzburg: University of Salzburg Austria, Master’s thesis
[24] Janičić, Predrag, Geometry constructions language, J. Autom. Reason., 44, 3-24 (2010) · Zbl 1185.68626
[25] Janičić, Predrag, GCLC — a tool for constructive euclidean geometry and more than that, (Iglesias, Andrés; Takayama, Nobuki, Mathematical Software - ICMS 2006. Mathematical Software - ICMS 2006, Lecture Notes in Computer Science, vol. 4151 (2006), Springer), 58-73 · Zbl 1230.51024
[26] Janičić, Predrag; Quaresma, Pedro, Automatic verification of regular constructions in dynamic geometry systems, (Botana, Francisco; Recio, Tomás, Automated Deduction in Geometry. Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 4869 (2007), Springer), 39-51 · Zbl 1195.68092
[27] Janičić, Predrag; Narboux, Julien; Quaresma, Pedro, The area method: a recapitulation, J. Autom. Reason., 48, 4, 489-532 (2012) · Zbl 1242.68281
[28] Jiang, Jianguo; Zhang, Jingzhong, A review and prospect of readable machine proofs for geometry theorems, J. Syst. Sci. Complex., 25, 4, 802-820 (2012) · Zbl 1291.68351
[29] Lemoine, Émile, Géométrographie ou Art des constructions géométriques. Number 18 in Scientia, Série Physico-Mathématique (Février 1902), C. Naud, Éditeur: C. Naud, Éditeur Paris
[30] (Lin, Fou-Lai; Hsieh, Feng-Jui; Hanna, Gila; de Villiers, Michael, Proceedings of the ICMI Study 19 Conference. Proceedings of the ICMI Study 19 Conference, Proof and Proving in Mathematics Education, vol. 1 (2009), The Department of Mathematics, National Taiwan Normal University)
[31] (Lin, Fou-Lai; Hsieh, Feng-Jui; Hanna, Gila; de Villiers, Michael, Proceedings of the ICMI Study 19 Conference: Proof and Proving in Mathematics Education, vol. 2 (2009), The Department of Mathematics, National Taiwan Normal University)
[32] Loria, Gino, La geometrografia e le sue trasfigurazioni, Period. Math., 3, 6, 114-122 (1908) · JFM 39.0559.01
[33] Mackay, John Sturgeon, The geometrography of Euclid’s problems, Proc. Edinb. Math. Soc., 12, 2-16 (1893) · JFM 25.0900.09
[34] Martin, George, Geometric Constructions (1998), Springer · Zbl 0890.51015
[35] McCallum, William, The Common Core State Standards in Mathematics, 547-560 (2015), Springer: Springer Cham
[36] Merikoski, Jorma K.; Tossavainen, Timo, Two approaches to geometrography, J. Geom. Graph., 13, 1, 15-28 (2010) · Zbl 1200.51012
[37] Morrow, Glenn R., Proclus, A Commentary on the First Book of Euclid’s Elements. Classics/History of Mathematics (1992), Princeton University Press
[38] Narboux, Julien, A graphical user interface for formal proofs in geometry, J. Autom. Reason., 39, 161-180 (2007) · Zbl 1131.68094
[39] Pąk, Karol, Improving legibility of formal proofs based on the close reference principle is NP-hard, J. Autom. Reason., 55, 3, 295-306 (Oct 2015)
[40] Pham, Tuan Minh; Bertot, Yves, A combination of a dynamic geometry software with a proof assistant for interactive formal proofs, Electron. Notes Theor. Comput. Sci., 285, 43-55 (2012), Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers (UITP10) · Zbl 1294.68126
[41] Pinheiro, Vergílio Athayde, Geometrografia 1 (1974), Gráfica Editora Bahiense
[42] Quaresma, Pedro, Thousands of geometric problems for geometric theorem provers (TGTP), (Schreck, Pascal; Narboux, Julien; Richter-Gebert, Jürgen, Automated Deduction in Geometry. Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 6877 (2011), Springer), 169-181 · Zbl 1350.68243
[43] Quaresma, Pedro, Towards an intelligent and dynamic geometry book, Math. Comput. Sci., 11, 3-4, 427-437 (Dec 2017)
[44] Quaresma, Pedro; Santos, Vanda, Visual geometry proofs in a learning context, (Neuper, Walther; Quaresma, Pedro, Proceedings of ThEdu’15. Proceedings of ThEdu’15, CISUC Technical Reports, vol. 2016001 (2016), CISUC), 1-6
[45] Quaresma, Pedro; Santos, Vanda; Baeta, Nuno, Exchange of geometric information between applications, (Quaresma, Pedro; Neuper, Walther, ThEdu’17 PostProceedings. ThEdu’17 PostProceedings, EPTCS, vol. 267 (2018), Open Publishing Association), 108-119
[46] Quaresma, Pedro; Santos, Vanda; Marić, Milena, WGL, a web laboratory for geometry, Edu. Inf. Technol., 23, 1, 237-252 (Jan 2018)
[47] Richter-Gebert, Jürgen; Kortenkamp, Ulrich, The Interactive Geometry Software Cinderella (1999), Springer · Zbl 0926.51002
[48] Rivera, Ferdinand D., Teaching to the Math Common Core State Standards (2013), Sense Publishers
[49] Rowe, Mary Budd, Wait-time and Rewards as Instructional Variables: Their Influence on Language, Logic, and Fate Control (1972), National Association for Research in Science Teaching, Technical report
[50] Santos, Vanda; Quaresma, Pedro; Campos, Helena; Marić, Milena, Web geometry laboratory: case studies in Portugal and Serbia, Interact. Learn. Environ., 26, 1, 3-21 (2018)
[51] Sidoli, Nathan, Uses of construction in problems and theorems in Euclid’s elements I-VI, Arch. Hist. Exact Sci., 72, 4, 403-452 (2018) · Zbl 1397.01007
[52] Stahl, Robert J., Using “Think-Time” and “Wait-Time” Skillfully in the Classroom (1994), Technical report, ERIC Digest
[53] Stojanović, Sana; Pavlović, Vesna; Janičić, Predrag, A coherent logic based geometry theorem prover capable of producing formal and readable proofs, (Schreck, Pascal; Narboux, Julien; Richter-Gebert, Jürgen, Automated Deduction in Geometry. Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 6877 (2011), Springer: Springer Berlin, Heidelberg), 201-220 · Zbl 1252.68264
[54] UNESCO, International Standard Classification of Education: ISCED 2011 (2012), UIS: UIS Montreal, Quebec
[55] Usiskin, Zalman, van Hiele Levels and Achievement in Secondary School Geometry (1982), University of Chicago, Technical report
[56] Wang, Ke; Su, Zhendong, Automated geometry theorem proving for human-readable proofs, (Proceedings of the 24th International Conference on Artificial Intelligence. Proceedings of the 24th International Conference on Artificial Intelligence, IJCAI’15 (2015), AAAI Press), 1193-1199
[57] Wiedijk, Freek, The de Bruijn factor, (Poster at International Conference on Theorem Proving in Higher Order Logics. Poster at International Conference on Theorem Proving in Higher Order Logics, TPHOL2000, Portland, Oregon, USA, 14-18 August 2000 (2000))
[58] Wu, Hung-Hsi, Teaching geometry according to the common core standards (2012)
[59] Ye, Zheng; Chou, Shang-Ching; Gao, Xiao-Shan, Visually dynamic presentation of proofs in plane geometry: Part 1. Basic features and the manual input method, J. Autom. Reason., 45, 3, 213-241 (October 2010)
[60] Ye, Zheng; Chou, Shang-Ching; Gao, Xiao-Shan, Visually dynamic presentation of proofs in plane geometry: Part 2. Automated generation of visually dynamic presentations with the full-angle method and the deductive database method, J. Autom. Reason., 45, 3, 243-266 (October 2010)
[61] Ye, Zheng; Chou, Shang-Ching; Gao, Xiao-Shan, An introduction to java geometry expert, (Sturm, Thomas; Zengler, Christoph, Automated Deduction in Geometry. Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 6301 (2011), Springer: Springer Berlin Heidelberg), 189-195 · Zbl 1302.68247
[62] Zhang, Jing-Zhong; Chou, Shang-Ching; Gao, Xiao-Shan, Automated production of traditional proofs for theorems in Euclidean geometry i. The Hilbert intersection point theorems, Ann. Math. Artif. Intell., 13, 1-2, 109-137 (Mar 1995)
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.