Abstract
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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
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)
Bertot, Y., Guilhot, F., Pottier, L.: Visualizing geometrical statements with GeoView. Electronic Notes in Theoretical Computer Science 103, 49–65 (2004)
Botana, F., Valcarce, J.L.: A dynamic-symbolic interface for geometric theorem discovery. Computers and Education 38, 21–35 (2002)
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)
Davenport, J.H.: On writing OpenMath content dictionaries. SIGSAM Bulletin 34(2), 12–15 (2000)
DIMACS: Satisfiability suggested format (May 1993), ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc/
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)
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)
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)
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)
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
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)
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)
Kapur, D.: Using Gröbner bases to reason about geometry problems. Journal of Symbolic Computation 2(4), 399–408 (1986)
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)
Narboux, J.: A graphical user interface for formal proofs in geometry. Journal of Automated Reasoning 39, 161–180 (2007)
Oracle: MySQL 5.5 Reference Manual, 5.5 edn. (January 2011), revision: 24956
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)
Quaresma, P., Janičić, P.: Geothms – a Web System for Euclidean Constructive Geometry. Electronic Notes in Theoretical Computer Science 174(2), 35–48 (2007)
Richter-Gebert, J., Kortenkamp, U.: The Interactive Geometry Software Cinderella. Springer, Heidelberg (1999)
Sutcliffe, G.: The TPTP problem library and associated infrastructure. Jounal of Automated Reasoning 43(4), 337–362 (2009)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Quaresma, P. (2011). Thousands of Geometric Problems for Geometric Theorem Provers (TGTP). In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds) Automated Deduction in Geometry. ADG 2010. Lecture Notes in Computer Science(), vol 6877. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25070-5_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-25070-5_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25069-9
Online ISBN: 978-3-642-25070-5
eBook Packages: Computer ScienceComputer Science (R0)