Un exemple d'explication de preuve formelle en langue naturelle

1) Introduction

   Je suis actuellement en train de finir une thèse en informatique. Je travaille à l'INRIA sous la direction de Gilles Kahn. Le sujet de ma thèse est « Explication Textuelle de Preuves ». J'ai souvent l'occasion de me rendre compte qu'il est très difficile d'expliquer ce que cela signifie aux personnes qui sont sont pas du domaine. Ces quelques pages sont motivées par le fait que ces personnes représentent l'immense majorité de la population. Il s'agit donc d'une tentative pour leur donner un aperçu de mon travail.

   Les preuves formelles sont des preuves mathématiques au sens usuel du mot. Ce qui les distingue des autres preuves est qu'elles ont la particularité d'être codées de façon à pouvoir être vérifiées automatiquement. Le mathématicien qui a défini une preuve formelle n'a plus à s'inquiéter de savoir s'il a oublié un cas ou s'il a fait une erreur de raisonnement. Une fois la preuve réalisée, un programme informatique peut s'assurer que la preuve ne comporte aucune erreur.

   Ces preuves formelles sont écrites de façon extrêmement rigoureuses. Elles doivent toutes respecter une certains nombre de règles sous peine d'être rejetées par la machine. Il existe plusieurs ensembles de règles qui définissent chacun une famille de preuve. Un tel ensemble est appelé formalisme. Celui que j'étudie s'appelle le Calcul des Constructions.

   Dans ce formalisme, les preuves ne sont pas écrites à la main. Elles sont réalisées inter-activement à l'aide d'un logiciel (j'utilise le logiciel Coq). Un inconvénient de ce formalisme est que les preuves sont représentées à l'aide d'un codage. Ce codage est conçu pour « pour un ordinateur » et est à peu près illisible « pour un être humain ». Le but de ma thèse est tout simplement de définir un programme qui prenne en entrée une preuve écrite à l'aide de ce codage, et qui rende en sortie une représentation en français de cette preuve.

  Je ne chercherai pas ici à expliquer ce programme mais simplement à donner une idée de ce qu'il fait. J'ai choisi un petit exemple de preuve, et je montre par améliorations successives les textes que l'on obtenir. (Cliquez sur Suite)

Yann Coscoy