Abstract
The pursuit of an AI 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 a computational application, a “book” of the future.
In the geometry book of the future 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 ask for proof hints. The book should also provide interactive exercises with automatic correction.
To fulfil such a goal the development of an open library of geometry automated theorem provers with a carefully design application interface protocol, must be considered. This would allow to link computer platforms for geometry with theorem provers, providing the automatic deduction capabilities for the AI Geometry Book.
Access provided by CONRICYT-eBooks. Download conference paper PDF
Similar content being viewed by others
Keywords
- Geometry Book
- Automated Geometry Theorem Proving (GATPs)
- Automated Deduction Methods
- Full-angle Method
- GeoGebra
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
1 Introduction
The geometry book of the future should be intelligent, correct, visual, adaptive, and collaborative in its production and use. Although the previous efforts and achievements help set aside many obstacles on the way to an intelligent geometry book, all the approaches, methods, techniques, basic tools, and systems, are still developed, applied, and conceived in separated, and relatively small, circles [13, 19].
When considering the application of automated reasoning in a learning context two, somehow opposing, goals are to be considered: efficiency and readability of the proofs. Whenever the help of the computer is considered, the user wants a fast and friendly answer [6].
Overall, the existing methods for automated theorem proving and discovering in geometry are very efficient and, in some cases, providing an output that can be used in a learning context. However, finding a method/implementation capable of both (fast and friendly) is only possible for a small number of cases. There is still a lot of room for further improvements [3].
Automated deduction methods can be more tightly integrated within interactive theorem provers and dynamic geometry [8, 9]. Automated deductions methods are currently unable to produce guidance and explanations for educational purposes. New techniques are needed involving synthetic geometry, formalisation techniques and artificial intelligence [2, 4, 5, 16].
Computer checking of geometric proofs has been addressed in the literature but: current formal proofs are not readable, natural and visual languages should be connected with formal deductions; several foundations of geometry and automated theorem provers are available, but all connections between them have not been obtained; the editing of a pedagogical corpus from formalisation have not been studied deeply enough [4, 7, 10, 20, 21].
Building on the work already developed in the systems: OpenGeoProver (OpenGeoProver) an open source project implementation of GATPs [1, 2]; the Thousand of Geometric problems for geometric Theorem Provers (TGTP) a problem repository and test bench [12]; and the standardised format for constructions and conjectures in geometry, i2gatp [14], we intend to extend and integrate these projects, providing deductive services to other applications.
The immediate program include the development/implementation of new methods to incorporate into the OpenGeoProver; finalising the standard format i2gatp to be able to define a programming protocol between OpenGeoProver and third-party programs; extend the platform TGTP in such a way that it can become the base for a competition between GATPs developed by the scientific community, to boost the improvement of methods/implementations.
Overview of the Paper. This paper is organised as follows: In Sect. 2 the current status and future developments of OpenGeoProver are described. In Sect. 3, the TGTP platform is described and the goal for a future competition between GATPs are set. In Sect. 4 the common format i2gatp is described and future developments are foreseen. In Sect. 5 the integration issues are discussed. In Sect. 6 some final remarks are drawn.
2 Open Geometry Prover
The OpenGeoProverFootnote 1 is an open source project, aiming to implement various geometry automated theorem provers (GATPs). It can be used as a stand-alone tool but can also be integrated into other geometry tools, such as dynamic geometry software, e.g., work is being made to integrate OpenGeoProver with GeoGebra [2]. In its current state, OpenGeoProver implements two algebraic methods, the Wu’s method and the Gröbner basis method, as well as one semi-synthetic method, the area method. Some initial work on the implementation of the full-angle method was already done [1].
As future developments we have: the implementation of new methods, finishing the work done with full-angle method, implementation of the deductive databases method, among others; the design of an application programming interface (API), allowing the different implemented GATPs to be easily used by other programs; write an extensive documentation, with a special care in the description of the API.
The OpenGeoProver will constitute an excellent mean to provide automated reasoning resources to the AI Geometry Book.
3 The TGTP Platform
Thousands of Geometric problems for geometric Theorem Provers (TGTP) is a Web-based library of problems in geometry, a comprehensive common library of problems with a significant size and unambiguous reference mechanism, easily accessible to all researchers in the automated reasoning in geometry community. It share the database of problems with the GeoThms, a Web-based framework for exploring geometrical knowledge that integrates Dynamic Geometry Software (DGS), Automatic Theorem Provers (ATP), and a repository of geometrical constructions, figures and proofs [5, 12].
One of the main motivations in building TGTP is to support the testing and evaluation of geometric automated theorem proving (GATP) systems. Providing a common library of problems for the testing of GATPs it will allow the pursue of the development of better methods/implementations.
Along the lines of the competition CASC [18], the conception and operationalization of a competition among GATPs is part of the future developments for the TGTP, it will allow the development of better methods/implementations, but will also push in the direction of a better interface between the geometric information and the programs that can use the information.
For the AI Geometry Book a repository such as TGTP is of extreme importance, it will constitute a source of valuable information to enrich the “book”.
4 The i2gatp Common Format
The i2gatp format is an extension of the i2g (Intergeo) common format aimed to support conjectures and proofs produced by geometric automatic theorem provers. The goal in building such a format is to provide a communication channel between different tools from the field of geometry, allowing linking such tools, as well as allowing the use of geometric knowledge kept in different repositories [14, 17].
The i2gatp format is a combination of four XSD files: information.xsd, with all the meta-information regarding the conjecture; intergeo.xsd, the Intergeo i2g format, for the description of geometric constructions; conjecture.xsd, the translation of geocons.dtd to the XSD format [11]; proofInfo.xsd, the meta-information regarding the proof generated by a given GATP on a given computing platform..
The i2gatp container is an extension of the i2g container. In addition to the information in the i2g container, all the information regarding the geometric conjecture and all the proofs attempts are kept in the i2gatp container.
The i2gatp library is an open source projectFootnote 2, to support the writing of filters from/to the i2gatp container and different geometric computation tools.
The i2gatp library will enable to specify an API, opening the possibility of geometric information interchange and the use of the GATPs in OpenGeoProver (and others, supporting the i2gatp format) and also the information contained in TGTP.
5 Deductive Tools in an AI Geometry Book
The integration that can be seen in systems like GeoThms, GeoGebra, Cinderella, JGEX, GCLC and GeoProof [2, 4, 5, 10, 16, 21], should be used as an inspiration to the AI Geometry Book.
The AI Geometry Book should be able to interface with repositories of geometric information and with DGSs and GATPs. Using the i2gatp common format as interface we could include deductive services via the OpenGeoProver and information via the TGTP repository.
Another two development that the author and other researcher are working on are: a taxonomy for geometric problems allowing to adjust the queries to each and every user [15]; a semantic search mechanism that will allow to search for geometric information in a geometric fashion.Footnote 3
6 Conclusions and Future Work
The pursuit of an AI Geometry Book—where the “book” is understood as a computation platform that will extend the concept of (non-digital) object of study, a repository of (non-digital) knowledge, to the digital world—needs the use of many AI techniques. AI is needed for the automatic deduction, for the adaptation to the user’s profiles, for the search of information.
Some of this issue are already, partially, solved, e.g. there are already many efficient GATPs, but the integration of all the “players” in such a way that a AI Geometry Book can be built is still to be done. As described above we are working on those issues, trying to integrate OpenGeoProver with TGTP through the i2gatp common format, and also on some issued related with the usability of such integrated platform, i.e. the adaptability and the semantic geometric search.
Notes
- 1.
- 2.
- 3.
Geometric Figure Mining via Conceptual Graphs, Yannis Haralambous and Pedro Quaresma, submitted to ADG2018.
References
Baeta, N., Quaresma, P.: The full angle method on the OpenGeoProver. In: Lange, C., et al. (eds.) MathUI, OpenMath, PLMMS and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, No. 1010 in CEUR Workshop Proceedings, Aachen (2013). http://ceur-ws.org/Vol-1010/paper-08.pdf
Botana, F., et al.: Automated theorem proving in Geogebra: current achievements. J. Autom. Reason. 55(1), 39–59 (2015). https://doi.org/10.1007/s10817-015-9326-4
Chou, S.C., Gao, X.S.: Automated reasoning in geometry. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 707–749. Elsevier Science Publishers B.V., San Diego (2001)
Janičić, P.: GCLC—a tool for constructive euclidean geometry and more than that. In: Iglesias, A., Takayama, N. (eds.) ICMS 2006. LNCS, vol. 4151, pp. 58–73. Springer, Heidelberg (2006). https://doi.org/10.1007/11832225_6
Janičić, P., Quaresma, P.: System description: GCLCprover + geoThms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 145–150. Springer, Heidelberg (2006). https://doi.org/10.1007/11814771_13
Jiang, J., Zhang, J.: A review and prospect of readable machine proofs for geometry theorems. J. Syst. Sci. Complex. 25(4), 802–820 (2012). https://doi.org/10.1007/s11424-012-2048-3
Matsuda, N., Vanlehn, K.: Gramy: a geometry theorem prover capable of construction. J. Autom. Reason. 32, 3–33 (2004)
Moraes, T.G., Santoro, F.M., Borges, M.R.: Tabulæ: educational groupware for learning geometry. In: Fifth IEEE International Conference on Advanced Learning Technologies, ICALT 2005, pp. 750–754, July 2005. https://doi.org/10.1109/ICALT.2005.251
Moriyón, R., Saiz, F., Mora, M.: GeoThink: an environment for guided collaborative learning of geometry. In: Sánchez, J. (ed) Nuevas Ideas en Informática Educativa, Santiago de Chile, vol. 4, pp. 200–208 (2008)
Narboux, J.: A graphical user interface for formal proofs in geometry. J. Autom. Reason. 39, 161–180 (2007). https://doi.org/10.1007/s10817-007-9071-4
Quaresma, P., Janičić, P., Tomašević, J., Vujošević-Janičić, M., Tošić, D.: XML-bases format for descriptions of geometric constructions and proofs. In: Communicating Mathematics in the Digital Era, pp. 183–197. A. K. Peters Ltd., Wellesley (2008)
Quaresma, P.: Thousands of geometric problems for geometric theorem provers (TGTP). In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) ADG 2010. LNCS (LNAI), vol. 6877, pp. 169–181. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25070-5_10
Quaresma, P.: Towards an intelligent and dynamic geometry book. Math. Comput. Sci. 11(3), 427–437 (2017). https://doi.org/10.1007/s11786-017-0302-8
Quaresma, P., Baeta, N.: Current status of the I2GATP common format. In: Botana, F., Quaresma, P. (eds.) ADG 2014. LNCS (LNAI), vol. 9201, pp. 119–128. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21362-0_8
Quaresma, P., Santos, V., Graziani, P., Baeta, N.: Taxonomies of geometric problems. J. Symb. Comput. (2018, Submitted)
Richter-Gebert, J., Kortenkamp, U.: The Interactive Geometry Software Cinderella. Springer, Heidelberg (1999)
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). http://i2geo.net/xwiki/bin/view/I2GFormat/
Sutcliffe, G.: The 5th IJCAR automated theorem proving system competition - CASC-J5. AI Commun. 24(1), 75–89 (2011). http://dl.acm.org/citation.cfm?id=1937696.1937700
Wang, D., Chen, X., An, W., Jiang, L., Song, D.: OpenGeo: an open geometric knowledge base. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 240–245. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44199-2_38
Wang, K., Su, Z.: Automated geometry theorem proving for human-readable proofs. In: Proceedings of the 24th International Conference on Artificial Intelligence, IJCAI 2015, pp. 1193–1199. AAAI Press (2015). http://dl.acm.org/citation.cfm?id=2832249.2832414
Ye, Z., Chou, S.-C., Gao, X.-S.: An introduction to Java geometry expert. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS (LNAI), vol. 6301, pp. 189–195. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21046-4_10
Acknowledgements
Financed by national funding via the Foundation for Science and Technology and by the European Regional Development Fund (FEDER), through the COMPETE 2020 – Operational Program for Competitiveness and Internationalisation (POCI).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Quaresma, P. (2018). Automatic Deduction in an AI Geometry Book. In: Fleuriot, J., Wang, D., Calmet, J. (eds) Artificial Intelligence and Symbolic Computation. AISC 2018. Lecture Notes in Computer Science(), vol 11110. Springer, Cham. https://doi.org/10.1007/978-3-319-99957-9_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-99957-9_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-99956-2
Online ISBN: 978-3-319-99957-9
eBook Packages: Computer ScienceComputer Science (R0)