Artificial Intelligence
Natural language processing
Semantic web

Creation of a proof generator for high school geometry problems that simulates the resolution process of a student, for the tutor software QED-Tutrix.

Student: Ludovic Font

Supervisor: Michel Gagnon

Co-supervisor(s): Philippe R. Richard (U. de M.)

The tutor software QED-Tutrix provides to high school students an interface to solve geometry proof problems, including a tutoring system to help them during the whole resolution process. This tutoring requires the anticipation of the various proofs the student could write, and therefore an a priori knowledge of all the possible proofs for a given problem. The manual encoding by an expert of this knowledge is particularly tedious and time-consuming. We therefore have the goal to automate this process as much as possible, by implementing an automated proof generator that generates all the proof a student could have written.