Automating the Generation of High School Geometry Proofs using Prolog in an Educational Context
This addresses the need for intelligent tutor systems in mathematics education to provide relevant help by anticipating student steps, though it appears incremental as it builds on existing logic programming approaches.
The paper tackled the problem of automating geometry proof generation for high school students by developing a Prolog-based theorem prover that produces proofs mimicking student reasoning, resulting in a system capable of generating complete sets of proofs.
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.