Abstract FR:

L'execution etendue generalise l'execution de prolog a des buts implicatifs. Un but implicatif est une implication entre deux conjonctions d'atomes qui contient des variables universelles et existentielles. L'extraction d'un programme a partir d'une preuve par execution etendue consiste a prouver un but implicatif initial et a extraire de cette preuve un programme logique. Le programme extrait calcule les variables existentielles en fonction des variables universelles et verifie des proprietes de correction partielle et de terminaison par rapport au but initial. La transformation de programmes consiste a remplacer un programme par un autre programme qui lui est equivalent ou qui le specialise. La methode de transformation par pliage/depliage permet de transformer des programmes recursifs logiques et preserve l'equivalence entre les programmes