TGTP - Thousand of Geometric problems for Theorem Provers

Authors

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 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.

Keywords

Library of problems in geometry; Geometric Automated Theorem Proving

Subject

geometric automated deduction

Conference

Workshop on Automated Deduction in Geometry, July 2011