Abstract FR:

La notion de preuves en programmation logique est examinee a deux niveaux differents. D'un point de vue externe, la theorie classique de la programmation logique est completement formalisee dans le calcul des constructions inductives. Apres avoir envisage le probleme de la definition de fonctions partielles dans un systeme dans lequel seules les fonctions totales sont representables, l'unification est obtenue en reutilisant une preuve formelle existante portant sur un sur-ensemble des termes. Les proprietes fondamentales de la sld-resolution sont alors formalisees. Le niveau de detail impose par la mecanisation des preuves considerees a mis en relief la complexite cachee de certaines preuves : le mecanisme de renommage est traite de maniere explicite, transformant ainsi certaines certitudes theoriques en realites. D'un point de vue interne, les preuves sld, finies ou infinies, sont comparees a celles que l'on peut obtenir, par induction ou par co-induction, a partir des clauses d'un programme logique vues comme des regles d'inference. Dans le cas fini la correspondance est complete (ce que calcule un programme est prouvable) tandis que dans le cas infini, certains objets non calculables sont toutefois prouvables. Les proprietes classiques des definitions co-inductives et la comparaison de certaines derivations infinies a des termes de preuve d'un type co-inductif, se revelent utiles tant pour expliquer les resultats d'incompletude d'approches existantes que pour definir une semantique valide et complete pour une classe de derivation infinies (precisement celles qui ne construisent pas de termes infinis).