Le but est d'établir les bases logiques de la programmation logique : certaines preuves peuvent calculer quelque chose, et l'exploitation de cette idée conduit à des langages de programmation, Prolog et ses prolongements (contraintes, concurrence, logique linéaire, ordre supérieur). Contenu : Calcul des séquents classiques : élimination des coupures - théorème de Herbrand - preuves constructives - preuves uniformes et programmes logiques. Contraintes symboliques : unification sur les termes finis et rationnels, résolution par transformations de systèmes. Interprétations et contraintes : un schéma général de résolution de contraintes : exemples (Prolog, CLP(R), CAL) Le non-déterminisme : contrôle et synchronisation des coroutines - la programmation logique concurrente. Extensions logiques et applications : formules de Harrop, ordre supérieur et spécification de systèmes logiques - logique linéaire et traitement des ressources : exemples (Lambda-Prolog, Elf, Lolli).
Bibliographie :
J. Gallier,Constructive Logics, University of Pennsylvania, 1992.
R.Lalement,Logique, réduction, résolution, Etudes et recherches en informatique. Masson, 1990.
V.Saraswat, Concurrent Constraint Programming, The MIT Press, 1993.