Ce document académique correspond à une dissertation soutenue en avril 2001 à la Technische Universität Graz, en Autriche, par Walther A. Neuper. Intitulée Reactive User-Guidance by an Autonomous Engine Doing High-School Math, cette recherche s'intéresse à l'intégration des outils informatiques dans l'enseignement secondaire des mathématiques, en particulier face aux limites des systèmes de calcul formel (CAS) traditionnels.
L'auteur y analyse l'impact de l'introduction de l'informatique en classe, soulignant d'une part la motivation qu'elle apporte aux élèves et aux enseignants, mais pointant d'autre part les risques d'une utilisation superficielle où les compétences fondamentales de calcul et de modélisation sont éclipsées par de simples pressions de boutons.
Le projet présenté vise à concevoir un composant logiciel intermédiaire, désigné sous le terme de « tuteur », capable de réintroduire le mode étape par étape dans la résolution des problèmes mathématiques. Ce tuteur ne se contente pas d'afficher un résultat global : il est conçu pour assister les élèves dans toutes les phases du travail, à savoir la modélisation, la spécification et la résolution proprement dite.
Le travail repose sur plusieurs apports originaux combinant des concepts issus de la démonstration automatique, de la compilation et de l'interaction homme-machine :
Le document est divisé en plusieurs chapitres principaux qui vont de la motivation didactique initiale jusqu'à la mise en œuvre technique et aux études de cas. Après une analyse critique des logiciels existants (systèmes de calcul formel, assistants de preuve, solveurs de contraintes), l'auteur détaille l'architecture de son moteur mathématique et les fondements formels du système, s'appuyant notamment sur l'assistant de preuve Isabelle.
La dernière partie de la thèse regroupe des études de cas pratiques, explorant la capacité d'Isabelle à effectuer des calculs de niveau secondaire, la gestion de hiérarchies de sous-problèmes pour la résolution d'équations, ainsi qu'un panorama complet des sujets de mathématiques du secondaire autrichien abordés par la réécriture de termes.
Le tuteur a pour but d'offrir une assistance interactive aux élèves du secondaire, en combinant la rigueur logique des démonstrateurs de théorèmes et la flexibilité d'un accompagnement pédagogique pas à pas, afin de pallier les insuffisances des logiciels de calcul formel classiques.
L'implémentation du prototype s'appuie principalement sur l'assistant de preuve Isabelle, développé en langage SML (Standard ML), et intègre des réflexions sur l'interactivité inspirées des interfaces modernes.
Ce travail s'adresse aux chercheurs, enseignants et étudiants en informatique, en didactique des mathématiques et en génie logiciel intéressés par l'intelligence artificielle appliquée à l'éducation.
Télécharger Dissertation sur l'aide interactive en mathématiques par Walther A. Neuper pdf
