Génération automatique de preuves pour un logiciel tuteur en géométrie

Le logiciel QED-Tutrix est un tuteur intelligent qui offre un cadre aidant les élèves de secondaire à résoudre des problèmes de géométrie. Une de ses caractéristiques fondamentales est l'aspect tuteur, qui accompagne l'élève dans sa résolution du problème, et l'aide à avancer en cas de blocage par le biais de messages, personnalisés selon son avancement dans la preuve. Une autre de ses caractéristiques est de rester proche de la façon dont un élève résoudrait le problème avec un papier et un crayon, et, par conséquent, lui permet d'explorer la construction de sa preuve dans l'ordre de son choix. En d'autres termes, si le premier instinct de l'élève est de remarquer une caractéristique de la situation géométrique n'étant ni un conséquent direct des hypothèses, ni un élément directement nécessaire à la conclusion, QED-Tutrix lui permet de commencer à résoudre le problème à partir de ce résultat intermédiare. Ces deux caractéristiques créent une difficulté importante. En effet, le logiciel doit fournir une aide personnalisée selon l'avancement de l'élève, qui peut contenir des éléments de preuve très variés et sans nécessairement de rapport direct entre eux, pouvant par exemple appartenir à plusieurs chemins de preuve distincts. Par conséquent, le logiciel doit connaître à l'avance les différents chemins de résolution possibles pour chaque problème, et être capable d'analyser ces chemins pour déterminer dans quelle direction l'élève se dirige. Pour résoudre cet enjeu, le logiciel associe à chaque problème une structure de données, nommée le graphe HPDIC et présentée plus en détail dans les sections centrales de ce document, qui permet de représenter sous forme de graphe toutes les preuves possibles pour un problème donné. Ainsi, il devient possible d'analyser finement l'avancement de l'élève dans sa résolution du problème, et ce quel que soit l'ordre dans lequel il a fourni les éléments de la preuve.