Contributions à la sémantique de la programmation logique

La notion de preuves en programmation logique est examinée à deux niveaux différents. D'un point de vue externe, la "théorie classique" de la programmation logique est complètement formalisée dans le calcul des constructions inductives. Après avoir envisagé le problème de la définition de fonctions partielles dans un système dans lequel seules les fonctions totales sont représentables, l'unification est obtenue en réutilisant une preuve formelle existante portant sur un sur-ensemble des termes. Les propriétés fondamentales des SLD-résolution sont alors formalisées. Le niveau de détail imposé par la mécanisation des preuves considérées a mis en relief la complexité cachée de certaines preuves: le mécanisme de renommage est traité de manière explicite, transformant ainsi certaines certitudes théoriques en réalités. D'un point de vue interne, les preuves SLD,finies ou infinies, sont comparées à celles que l'on peut obtenir, par induction ou par co-induction, à partir des clauses d'un programme logique vues comme des règles d'inférence. Dans le cas fini la correspondance est complète ("ce que calcule un programme est prouvable") tandis que dans le cas infini, certains objets non calculables sont toutefois prouvables. Les propriétés classiques des définitions co-inductives et la comparaison de certaines dérivations infinies à des termes de preuve d'un type co-inductif, se révèlent utiles tant pour expliquer les résultats d'incomplétude d'approches existantes que pour définir une sémantique valide et complète pour une classe de dérivations infinies (précisement celles qui ne construisent pas de termes infinis).(résumé de l'auteur