TGTP - Thousand of Geometric problems for Theorem Provers



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 support the testing and evaluation of geometric automated theorem proving systems (GATP). For that propose TGTP provides a centralised common library of geometric problems with an already significant size but aiming to became large enough to ensure a meaningful system evaluations and comparisons. TGTP provides also a Workbench were it is possible to evaluate a given GATP with any given conjecture.

TGTP is independent of any given GATP. For each problem and for the code for each GATP, whenever available is kept in the library. A common format for geometric conjectures, adding to 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 to an easy access to the information. All the information in the library, and also the supporting formats and tools are freely available.

TGTP aims, in a similar spirit of {em 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.


Library of problems in geometry; Geometric Automated Theorem Proving


geometric automated deduction


Workshop on Automated Deduction in Geometry, July 2011

Cited by

Year 2015 : 1 citations

 Chen, X., Song, D., & Wang, D. (2015). Automated generation of geometric theorems from images of diagrams. Annals of Mathematics and Artificial Intelligence, 74(3-4), 333-358.

Year 2014 : 3 citations

 Chen, Xiaoyu, Representation and automated transformation of geometric statements, JSSC 27,2. Doi: 10.1007/s11424-014-0316-0

 Chen, Xiaoyu and Song, Dan and Wang, Dongming, Automated generation of geometric theorems from images of diagrams, Annals of Mathematics and Artificial Intelligence, Springer 2014. DOI: 10.1007/s10472-014-9433-7

 Wang, Dongming and Chen, Xiaoyu and An, Wenya and Jiang, Lei and Song, Dan, OpenGeo: An Open Geometric Knowledge Base, LNCS 8592, Springer 2014. Doi: 10.1007/978-3-662-44199-2_38

Year 2013 : 1 citations

 Formalization and Specification of Geometric Knowledge Objects, X. Chen, D. Wang - Mathematics in Computer Science, 2013 - Springer

Year 2012 : 1 citations

 Xiaoyu Chen, Interfacing Euclidean Geometry Discourse with Diverse Geometry Software (Extended Abstract), Informatics Research Report, ADG2012, School of Informatics, University of Edinburgh, September 2012.