Thousands of Geometric Problems for Geometric Theorem Provers (TGTP)
Thousands of Geometric Problems for Geometric Theorem Provers (TGTP)
复制标题
DOI：
10.1007/978-3-642-25070-5_10
复制
发表时间：
2010-07
期刊：
影响因子：
--
通讯作者：
P. Quaresma
中科院分区：
文献类型：
--
作者：
P. Quaresma
Thousands of Geometric Problems for Geometric Theorem Provers（TGTP）是一个基于Web的几何问题库，其主要目的是为测试和评估几何自动定理证明系统（GATP）提供一个合适的环境。为了这个目的，TGTP提供了一个集中的几何问题的公共库，这些问题已经很大，但旨在变得足够大，以确保有意义的系统评估和比较。TGTP还提供了一个工作台，可以测试任何给定的几何猜想。TGTP独立于任何给定的GATP。对于每个问题，每个GATP的代码（只要可用）都保存在库中。正在开发一种通用的几何图形格式，扩展了i2g格式。这种通用格式，加上一个转换器列表，每个GATP一个，将允许测试库中的所有问题的所有GATP。TGTP结构良好，有文档记录，并具有强大的查询机制，允许轻松访问信息。该库中的所有信息，以及支持的格式和工具都是免费提供的。TGTP旨在与TPTP和其他库类似的精神，为几何界的自动推理提供一个全面且易于访问的GATP测试问题库。TGTP问题库的开发是一个正在进行的项目。
Thousands of Geometric problems for geometric Theorem Provers (TGTP) is a Web-based library of problems in geometry.The principal motivation in buildingTGTPis to create an appropriate context for testing and evaluating geometric automated theorem proving systems (GATP). For that purposeTGTPprovides 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.TGTPprovides also a workbench were it is possible to test any given geometric conjecture.TGTPis 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.TGTPis 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.TGTPaims, in a similar spirit ofTPTPand other libraries, to provide the automated reasoning in geometry community with a comprehensive and easily accessible library of GATP test problems. The development ofTGTPproblem library is an ongoing project.