Towards a Geometry Automated Provers Competition
This addresses the need for standardized evaluation and ranking of GATPs, particularly for educational applications, but is incremental as it focuses on competition design rather than new methods.
The paper proposes establishing a competition for geometry automated theorem provers (GATP) to create a test bench for developers to improve and rank existing methods, enabling clients like educational e-learning systems to choose the best implementation for specific uses.
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.