Jaume, Mathieu (1999) Contributions à la sémantique de la programmation logique. PhD thesis Informatique, ENPC - CERMICS Centre d'Enseignement et de Recherche en Mathématiques et Calcul Scientifique, ENPC p.206.
Full text available as:
|
|
Alternative Locations: http://cermics.enpc.fr/theses/index.html
Abstract
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)
| Item Type: | PhD Thesis (PhD) |
|---|---|
| Thesis Supervisor: | Lalement, René |
| Date: | January 1999 |
| Board of examiners: | Guessarian, Irène and Viguié Donzeau-Gouge, Véronique and Ridoux, Olivier and Bernot, Gilles and Dowek, Gilles |
| Discipline: | Informatique |
| Collection (Fonds): | ENPC |
| Institution: | ENPC |
| Department: | ENPC - CERMICS Centre d'Enseignement et de Recherche en Mathématiques et Calcul Scientifique |
| Subjects: | 2. Information and Communication Sciences and Technologies 1. Mathematics and Applications |
| ID Code: | 106 |
|---|---|
| Deposited By: | Jean-Gérard Pailloncy |
| Deposited On: | 02 May 2002 |
Repository Staff Only: edit this item