Recherche de preuves en $AF_2$ par codage dans une logique d'ordre supérieur

Jury (07 septembre 1994)

• Monique Grandbastien
• Didier Galmiche
• Dominique Mery
• Pierre Marquis
• Adam Cichon

Introduction

Depuis plusieurs années de nombreux travaux ont été consacrés à l’étude de la déduction de programmes dans un cadre logique en utilisant des techniques basées sur la transformation de preuves ou sur la démonstration de théorèmes. Nous considéreront ici cette deuxième technique avec une approche particulière, la programmation par preuves , utilisant une logique (intuitionniste) constructive, ainsi que ses applications à la programmation.

Différentes théories relatives à cette technique ont été développées, notamment la Théorie des Types de Martin-Löf (MLTT), le Calcul des Constructions (CC) et l’Arithmétique Fonctionnelle du second ordre ($AF_2$). Programmer dans un tel cadre logique consiste à donner une spécification formelle (ou proposition dans le système), à en construire une preuve, puis à extraire automatiquement de cette preuve un code exécutable en utilisant, par exemple, l’isomorphisme formulae as types de Curry-Howard. De ce fait, la notion de programmation se fonde sur la recherche de preuves en théorie des types. Certains résultats mathématiques nous permettent d’obtenir d’importantes propriétés telles que la correction et la terminaison des programmes ainsi synthétisés.

Dans le cadre de ce rapport, nous allons étudier la recherche de preuves dans la théorie $AF_2$. Cette logique a déjà été l’objet de nombreux travaux, notamment en ce qui concerne l’étude des liens entre preuves et programmes (les meilleures preuves ne donnent pas obligatoirement les meilleurs algorithmes) et l’automatisation de cette recherche de preuves (notions de tactiques, de plans de preuves et de $R$-preuves).

L’angle sous lequel nous allons aborder le problème de la recherche de preuves et de la synthèse de programmes en $AF_2$ est quelque peu particulier. Nous allons coder la logique $AF_2$ dans une autre logique d’ordre supérieur pour laquelle on sait définir des procédures de recherche de preuves qui reposent sur des classes de preuves complètes. Ceci est une approche complémentaire aux travaux cités ci-dessus. Elle doit permettre une meilleure compréhension de l’automatisation de la recherche de preuves. Nous étudierons la recherche de preuves dans la logique intuitionniste d’ordre supérieur $I$ pour laquelle ont éé présentées dans la notion de preuve uniforme (tout séquent ayant comme succédent une formule non atomique est la conclusion d’une règle d’introduction à droite) ainsi qu’une procédure de recherche complète (s’il existe une preuve, cette procédure la trouvera) mais non-déterministe associée. Notre objectif est donc de représenter la théorie $AF_2$ dans la logique $I$ afin de pouvoir utiliser des procédures de recherche sur les formules d’$AF_2$ ainsi codées. En étudiant les résultats de cette recherche de preuves par codage dans une autre logique, on devrait pouvoir définir directement pour $AF_2$ une notion de preuve canonique, comme celles reposant sur les preuves uniformes de $I$ ou bien d’autres, ainsi qu’une procédure de recherche de preuves (afin de pouvoir en extraire des programmes) correspondante.

[…]