Browse Theses

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.La difficulté devient alors de générer ce graphe pour chacun des problèmes que l'on souhaite ajouter au logiciel. À la première itération de développement, ces graphes étaient générés à la main par un des experts en didactique du projet. Cette procédure, convenable pour une petite quantité de problèmes, devient fastidieuse et peu appropriée lorsque l'on souhaite ajouter un grand nombre de problèmes. Il est donc rapidement devenu nécessaire d'automatiser ce processus. Bien que la démonstration automatique de théorème, ou Automated Theorem Proving (ATP), soit un domaine de recherche dynamique, les enjeux très spécifiques de ce projet rendent difficile l'utilisation de techniques ou outils existants. Cette difficulté est explorée en détail dans la revue de littérature, au chapitre 2.Par conséquent, nous avons opté pour créer notre propre générateur de preuves, afin de pouvoir ajuster son fonctionnement aux besoins, à la fois didactiques et techniques, du projet. Nous avons également choisi de créer cet outil en utilisant la programmation logique, plus précisément le langage Prolog, car le paradigme de la programmation logique est tout à fait approprié pour représenter des démonstrations mathématiques basées sur des inférences. En effet, les parallèles entre une preuve mathématique et la résolution d'une requête en programmation logique sont flagrants. Une preuve mathématique peut être vue comme une succession d'inférences, chacune constituée d'antécédents, d'une justification, qui peut être une définition, une propriété ou un théorème, et d'un conséquent. Le conséquent d'une inférence peut ensuite servir d'antécédent à une autre inférence, créant ainsi un chemin inférentiel partant des hypothèses du problème et arrivant à la conclusion attendue. En programmation logique, la base de connaissance contient des faits ("facts"). Ces faits permettent d'activer des règles ("rules") afin de générer de nouveaux faits, qui sont ensuite ajoutés à la base de connaissances, et permettront éventuellement d'activer de nouvelles règles. Le parallèle est aisé, en faisant correspondre les résultats mathématiques aux faits, les inférences aux applications de règles. La démonstration complète consiste alors à générer la conclusion du problème à partir de l'ensemble des faits représentant les hypothèses initiales.Fort de cette conviction, nous avons donc développé notre générateur de preuves en Prolog. Cet outil, à partir d'un ensemble de règles représentant les justifications mathématiques présentes au programme de géométrie du secondaire au Québec, et d'un ensemble d'hypothèses décrivant une situation géométrique, est capable de générer l'ensemble des informations qu'un élève de secondaire pourrait inférer. Ainsi, lorsque la situation géométrique correspond à un problème, le générateur de preuves fournit l'intégralité des preuves pour ce problème, sous la forme d'un graphe HPDIC, tel que mentionné précédemment.