|
Action Concertée Incitative Nouvelles Interfaces des Mathématiques |
|
|
Projet Mao -- Mathématiques assistées par ordinateur |
|
|
6- Les données méta-logiques
Notre assistant Coq ne s'occupe pas seulement de représenter les énoncés et leurs preuves, il représente aussi des objets méta-logiques dont le rôle est d'agir sur les énoncés et les preuves, en particulier tactiques et coercions. La deuxième chose que l'expérience nous a enseignée, c'est que la programmation d'une bibliothèque ne se limite pas aux définitions et aux théorèmes. Si l'on veut qu'une bibliothèque permette de faire des preuves faciles et rapides, il est impératif d'y inclure les données méta-logiques adéquates. C'est pourquoi nous attachons la plus grande importance au développement de tactiques spécifiques pour chaque structure de données que nous implémentons. Par exemple, nous fournissons une tactique pour les groupes destinée à dispenser l'utilisateur, dans la grande majorité des cas, d'invoquer explicitement des théorèmes de réécriture pour les expressions de groupe.
7- Notre communauté d'utilisateurs
Nous développons notre environnement comme un système-expert: nos conceptions sont guidées par l'expérience et les aspirations de ceux d'entre nous qui sont mathématiciens, et nous confrontons constamment nos choix à des utilisateurs hors de notre projet. Ces utilisateurs sont d'une part des étudiants et enseignants de première année, et d'autre part des doctorants, appelés à être de plus en plus nombreux. En effet, cette année, nous avons déjà introduit dans l'enseignement du DEUG MIAS de façon expérimentale et à dose homéopathique notre environnement, couplé avec le serveur WIMS, qui est lui aussi développé dans notre équipe. Et nous comptons passer à une utilisation beaucoup plus massive dès la prochaine rentrée. Il faut noter que les ressources requises en première année sont suffisamment modestes, et que notre interface permet déjà, à ce niveau, de faire les preuves ordinaires plus vite qu'on ne les ferait sans ordinateur. Parallèlement, nous recrutons des cobayes parmi les doctorants qui sont interessés à certifier une partie de leurs preuves. Dans la mesure où la certification n'est que partielle, on peut choisir dans chaque cas un terrain où le problème des ressources est surmontable. Il faut aussi souligner que le rapport de un à cent mentionné plus haut ne s'applique pas forcément au cas d'un doctorant, par exemple lorsque celui-ci doit mettre au point une preuve qu'il ne comprend pas trop bien. Pour le moment, nous avons quatre tels cobayes. (dernière mise à jour du site : 14 décembre 2004) |
|
|
|
|