Automating the Generation of High School Geometry Proofs using Prolog in an Educational Context

Ludovic Font
(École Polytechnique de Montréal)
Sébastien Cyr
(Université de Montréal)
Philippe R. Richard
(Université de Montréal)
Michel Gagnon
(École Polytechnique de Montréal)

When working on intelligent tutor systems designed for mathematics education and its specificities, an interesting objective is to provide relevant help to the students by anticipating their next steps. This can only be done by knowing, beforehand, the possible ways to solve a problem. Hence the need for an automated theorem prover that provide proofs as they would be written by a student. To achieve this objective, logic programming is a natural tool due to the similarity of its reasoning with a mathematical proof by inference. In this paper, we present the core ideas we used to implement such a prover, from its encoding in Prolog to the generation of the complete set of proofs. However, when dealing with educational aspects, there are many challenges to overcome. We also present the main issues we encountered, as well as the chosen solutions.

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. 1–16.
Published: 28th February 2020.

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