Return to search

Etude et Réalisation d'un Système d'Aide à la Mise au Point en Programmation Logique

L'apparition d'interprètes sur de gros systèmes, tels Prolog-Dec10, puis des premiers compilateurs Prolog basés sur le fonctionnement de la machine virtuelle de Warren contribuèrent à la renommée du langage ainsi qu'a sa diffusion dans les universités puis l'industrie comme un puissant langage de l'Intelligence Artificielle [Warren-77, 83]. Le langage Prolog est fondé sur une restriction de la logique du premier ordre : l'ensemble des clauses de Horn. Le fait d'utiliser la logique du premier ordre comme langage de programmation était révolutionnaire parce que, jusqu'en 1972, une des utilisations de la logique en informatique était pour écrire des spécifications formelles et déclaratives. Kowalski nous montre dans son papier sur ce langage [Kowalski-74] que la logique des clauses de Horn possède une interprétation opérationnelle qui la rend très efficace comme fondement d'un langage de programmation, puis il effectue une preuve de la complétude de la méthode de dérivation sur laquelle se fondent tous les interprètes Prolog. De plus, la définition d'une sémantique formelle d'un langage de programmation logique [Emden-Kowalski-76] permet de définir une sémantique du point fixe pour les programmes utilisant les clauses de Hom comme syntaxe formelle, mais elle permet aussi de démontrer qu'elle était identique au modèle minimal d'une sémantique opérationnelle. Cet aspect est aussi étudié dans le cadre de la norme Prolog en cours de rédaction [Deransart&all-85].

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00831323
Date25 April 1990
CreatorsDebarbieri, Christian
PublisherEcole Nationale Supérieure des Mines de Saint-Etienne, Université Jean Monnet - Saint-Etienne
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
TypePhD thesis

Page generated in 0.002 seconds