论文标题
进行几何自动掠夺竞赛
Towards a Geometry Automated Provers Competition
论文作者
论文摘要
几何形状自动化定理区域以大量的特定方法和实现，不同的方法（合成，代数，半合成）和不同的目标和应用（从人工智能领域的研究到教育中的应用）。 除了通常的效率度量（例如CPU时间）外，视觉和/或可读证明的可能性也是预期的输出，几何学自动化定理弃权（GATP）应测量。 GATP之间的竞争的实施将允许为GATP开发人员创建一个测试工作台，以改善现有竞争并提出新的测试。它还允许建立GATP的排名，该排名可以由“客户”（例如，教育电子学习系统的开发人员）使用，以选择给定预期用途的最佳实现。
The geometry automated theorem proving area distinguishes itself by a large number of specific methods and implementations, different approaches (synthetic, algebraic, semi-synthetic) and different goals and applications (from research in the area of artificial intelligence to applications in education). Apart from the usual measures of efficiency (e.g. CPU time), the possibility of visual and/or readable proofs is also an expected output against which the geometry automated theorem provers (GATP) should be measured. The implementation of a competition between GATP would allow to create a test bench for GATP developers to improve the existing ones and to propose new ones. It would also allow to establish a ranking for GATP that could be used by "clients" (e.g. developers of educational e-learning systems) to choose the best implementation for a given intended use.
