Towards a Geometry Automated Provers Competition

Nuno Baeta
(University of Coimbra)
Pedro Quaresma
(University of Coimbra)
Zoltán Kovács
(The Private University College of Education of the Diocese of Linz)

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.

In Pedro Quaresma, Walther Neuper and João Marcos: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software (ThEdu'19), Natal, Brazil, 25th August 2019, Electronic Proceedings in Theoretical Computer Science 313, pp. 93–100.
Published: 28th February 2020.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: