11) Conclusion

   Nous avons trouvé que traduire une preuve formelle en une forme facilement accessible à un mathématicien comporte essentiellement trois opérations : le décodage, la contraction et la présentation. Ceci est vrai en particulier pour la Calcul des Constructions, mais je pense c'est aussi le cas pour la plupart des preuves formelles. Détaillons maintenant chacune de ces opérations.

   Le décodage : Il s'agit ici de comprendre la façon dont sont codées les informations dans le formalisme (ici le Calcul des Constructions). C'est une opération purement technique qui doit être résolue en premier.

   La contraction : Les preuves formelles se particularisent par une abondance de détails et une forte lourdeur dans le raisonnement. Pour faire comprendre une preuve formelle à un être humain, il est nécessaire d'aller à l'essentiel. Donner trop de détails inutiles rend impossible la lecture d'une preuve. C'est à notre avis l'opération la plus difficile. Il n'y a pas de solution unique. C'est la qualité de cette opération qui fait toute la différence entre une explication utile et compréhensible est une explication confuse et inutilisable.

   La présentation : Nous appelons présentation proprement dite l'étape qui commence une fois la preuve décodée et contractée. À ce moment, nous savons exactement ce que nous allons dire, il ne s'agit plus que de l'écrire. C'est ici que nous utilisons le français. Comme pour la cas de la contraction il n'y a pas de solution unique. Le but de cette opération est d'obtenir un texte facile à lire. Une bonne présentation rend la lecture d'une preuve plus agréable et favorise la compréhension

   En guise de conclusion nous pouvons dire que j'espère vous avoir donné un aperçu de ce que j'entends par « Explication Textuelle de preuves ». Il ne s'agit pas, loin de là, de la seule façon d'aborder le problème, mais c'est l'approche que j'utilise dans mon travail de thèse. Si vous avez une remarque à faire, si vous voyez une faute d'orthographe, n'hésitez pas m'envoyer un message à l'adresse Yann.Coscoy@sophia.inria.fr.

Yann Coscoy