Thousands of geometric problems for geometric theorem provers (TGTP). (English) Zbl 1350.68243

Schreck, Pascal (ed.) et al., Automated deduction in geometry. 8th international workshop, ADG 2010, Munich, Germany, July 22–24, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-25069-9/pbk). Lecture Notes in Computer Science 6877. Lecture Notes in Artificial Intelligence, 169-181 (2011).
Summary: Thousands of Geometric problems for geometric Theorem Provers (TGTP) is a Web-based library of problems in geometry.
The principal motivation in building TGTP is to create an appropriate context for testing and evaluating geometric automated theorem proving systems (GATP). For that purpose TGTP provides a centralised common library of geometric problems with an already significant size but aiming to became large enough to ensure meaningful system evaluations and comparisons. TGTP provides also a workbench were it is possible to test any given geometric conjecture.
TGTP is independent of any given GATP. For each problem the code for each GATP (whenever available) is kept in the library. A common format for geometric conjectures, extending the i2g format, is being developed. This common format, plus a list of converters, one for each GATP, will allow to test all the GATPs with all the problems in the library.
TGTP is well structured, documented and with a powerful querying mechanism, allowing an easy access to the information. All information in the library, and also the supporting formats and tools are freely available.
TGTP aims, in a similar spirit of TPTP and other libraries, to provide the automated reasoning in geometry community with a comprehensive and easily accessible library of GATP test problems. The development of TGTP problem library is an ongoing project.
For the entire collection see [Zbl 1227.68009].


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
51-04 Software, source code, etc. for problems pertaining to geometry
Full Text: DOI


[1] Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, England (2010)
[2] Bertot, Y., Guilhot, F., Pottier, L.: Visualizing geometrical statements with GeoView. Electronic Notes in Theoretical Computer Science 103, 49–65 (2004)
[3] Botana, F., Valcarce, J.L.: A dynamic-symbolic interface for geometric theorem discovery. Computers and Education 38, 21–35 (2002)
[4] Buchberger, B., Craciun, A., Jebelean, T., Kovacs, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkranz, M., Windsteiger, W.: Theorema: Towards computer-aided mathematical theory exploration. Journal of Applied Logic 4(4), 470–504 (2006) · Zbl 1107.68095
[5] Davenport, J.H.: On writing OpenMath content dictionaries. SIGSAM Bulletin 34(2), 12–15 (2000)
[6] DIMACS: Satisfiability suggested format (May 1993), ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc/
[7] Egido, S., Hendriks, M., Kreis, Y., Kortenkamp, U., Marquès, D.: i2g Common File Format Final Version. Tech. Rep. D3.10, The Intergeo Consortium (2010)
[8] Fuchs, K., Hohenwarter, M.: Combination of dynamic geometry, algebra and calculus in the software system geogebra. In: Computer Algebra Systems and Dynamic Geometry Systems in Mathematics Teaching Conference 2004, pp. 128–133. Pécs, Hungary (2004)
[9] Gao, X.-S., Lin, Q.: MMP/Geometer - a Software Package for Automated Geometric Reasoning. In: Winkler, F. (ed.) ADG 2002. LNCS (LNAI), vol. 2930, pp. 44–66. Springer, Heidelberg (2004) · Zbl 1202.68378
[10] Hoos, H., Stützle, T.: SATLIB: An online resource for research on SAT. In: Gent, I.P., Maaren, H.V., Walsh, T. (eds.) SAT 2000, pp. 283–292. IOS Press, Amsterdam (2000) · Zbl 0979.68128
[11] Janičić, P., Narboux, J., Quaresma, P.: The Area Method: a recapitulation. Journal of Automated Reasoning 7 (to appear, 2011), doi:10.1007/s10817-010-9209-7 · Zbl 1242.68281
[12] 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) · Zbl 1230.51024
[13] 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) · Zbl 05528282
[14] Kapur, D.: Using Gröbner bases to reason about geometry problems. Journal of Symbolic Computation 2(4), 399–408 (1986) · Zbl 0629.68087
[15] Kortenkamp, U., Richter-Gebert, J.: Using automatic theorem proving to improve the usability of geometry software. In: Procedings of the Mathematical User-Interfaces Workshop 2004 (2004)
[16] Narboux, J.: A graphical user interface for formal proofs in geometry. Journal of Automated Reasoning 39, 161–180 (2007) · Zbl 1131.68094
[17] Oracle: MySQL 5.5 Reference Manual, 5.5 edn. (January 2011), revision: 24956
[18] 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. (2008)
[19] Quaresma, P., Janičić, P.: Geothms – a Web System for Euclidean Constructive Geometry. Electronic Notes in Theoretical Computer Science 174(2), 35–48 (2007) · Zbl 1278.68279
[20] Richter-Gebert, J., Kortenkamp, U.: The Interactive Geometry Software Cinderella. Springer, Heidelberg (1999) · Zbl 0926.51002
[21] Sutcliffe, G.: The TPTP problem library and associated infrastructure. Jounal of Automated Reasoning 43(4), 337–362 (2009) · Zbl 1185.68636
[22] Wang, D.: GEOTHER 1.1: Handling and Proving Geometric Theorems Automatically. In: Winkler, F. (ed.) ADG 2002. LNCS (LNAI), vol. 2930, pp. 194–215. Springer, Heidelberg (2004) · Zbl 1202.68390
[23] Wilson, S., Fleuriot, J.: Combining dynamic geometry, automated geometry theorem proving and diagrammatic proofs. In: Proceedings of the European Joint Conferences on Theory and Practice of Software (ETAPS) Satellite Workshop on User Interfaces for Theorem Provers (UITP). Springer, Heidelberg (2005)
[24] Wu, W.T.: The characteristic set method and its application. In: Gao, X.S., Wang, D. (eds.) Mathematics Mechanization and Applications, pp. 3–41. Academic Press, San Diego (2000)
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.