Séminaire Stéphanois de Mathématiques Accessibles

Philippe EZEQUEL (Laboratoire Hubert Curien)

Orateur : Philippe EZEQUEL (Laboratoire Hubert Curien)

Titre : Sémantique de la programmation logique

Résumé : "Il n'est pas nécessaire d'espérer pour entreprendre, ni de réussir pour persévérer" : même si Kurt Gödel a répondu négativement à la question posée par Hilbert concernant la possibilité de mécanisation des preuves en théorie des ensembles, on peut tout de même, dans le cadre plus restreint de la logique du premier ordre (dite aussi "des prédicats"), concevoir des machines universelles permettant de prouver des conséquences logiques d'une théorie donnée.

En se fondant sur les travaux de Jacques Herbrand et ceux d'Alan Robinson, Alain Colmerauer et Robert Kowalski ont, indépendamment, proposé un mécanisme de calcul de conséquences logiques, la programmation logique (dont le langage archétypal est Prolog). Il se pose alors le problème auquel sont confrontés tous les concepteurs de machines abstraites: que calcule-t-elle? La réponse est une définition de la sémantique dénotationnelle (cad comme point fixe d'un opérateur continu) des programmes logiques, en lien avec la sémantique logique des programmes.

L'exposé débutera par un rappel des notions de logiques nécessaires (et suffisantes, il n'est pas question d'être encyclopédique). Je montrerai ensuite le cheminement qui mène des formules logiques à la programmation logique, avec des exemples et des démonstrations de programmes (mais l'exposé ne sera pas un cours de programmation Prolog!).
Enfin j'exposerai la sémantique dénotationnelle de la programmation logique ainsi que les problèmes posés par la négation. 

forall