<  Retour au portail Polytechnique Montréal

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

Ludovic Font

Thèse de doctorat (2021)

Document en libre accès dans PolyPublie
[img]
Affichage préliminaire
Libre accès au plein texte de ce document
Conditions d'utilisation: Tous droits réservés
Télécharger (2MB)
Afficher le résumé
Cacher le résumé

Résumé

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.

Abstract

The QED-Tutrix project has the ultimate goal of creating, improving, and expanding the eponym tutor software, to accompany high school students in the resolution of geometry problems. Based on proven mathematics education theories, it has several distinctive characteristics. First, as a tutor software, the tutoring aspect is paramount. The virtual tutor, aptly named Professor Turing, is tasked with helping the student through the entire resolution process, from the exploration of the problem to the redaction of the proof. Second, the software as a whole stays close to the way students would typically solve a problem with paper and pencil, while adding digital tools to improve this process. This includes a dynamic geometry interface to explore the problem, a listing of available justifications, such as definitions or theorems, and a semi-automated redaction engine. Further, the student is allowed, like in real life, to construct the proof by adding elements in any order, for example by noticing a particular geometrical result on the figure, that is neither a hypothesis of the problem or its conclusion. It is possible in QED-Tutrix to begin the proof “in the middle”, by stating this particular result and working from there.These educational goals create interesting issues from a computer science point of view. Indeed, the tutoring is tailored to the exact point of the resultion reached by the student, and this point can be quite discontinuous since the elements of the resolution may have been entered in any order, can be unrelated, or pertain to different possible proofs of the problem. As a logical consequence, in order for the software to “know” what the student is doing and, mostly, what he or she is missing to complete the resolution, it is necessary to know, beforehand, all the possible proofs for the problem.

Département: Département de génie informatique et génie logiciel
Programme: Génie informatique
Directeurs ou directrices: Michel Gagnon et Philippe R. Richard
URL de PolyPublie: https://publications.polymtl.ca/9090/
Université/École: Polytechnique Montréal
Date du dépôt: 25 nov. 2021 14:34
Dernière modification: 22 avr. 2023 05:38
Citer en APA 7: Font, L. (2021). Génération automatique de preuves pour un logiciel tuteur en géométrie [Thèse de doctorat, Polytechnique Montréal]. PolyPublie. https://publications.polymtl.ca/9090/

Statistiques

Total des téléchargements à partir de PolyPublie

Téléchargements par année

Provenance des téléchargements

Actions réservées au personnel

Afficher document Afficher document