Unité d'enseignement M36 :

« Logique, déduction et programmation »

contenu mis à jour le 2007/10/15 16:00

Description

Crédits : 6

Lieu :  U.F.R. Sciences de Luminy et U.F.R. M.I.M.

Pré-requis : 2M5IN22

Semestre :  S2

Cours/TD/TP : 20h/20h/20h

Code APOGEE (U2) : C51IN36

Code APOGEE (U1) : 2INF14

Responsables :

Résumé : Ce cours a pour objectif de donner aux étudiants les bases de la logique formelle à partir de l'étude de la logique propositionnelle et de la logique du premier ordre. On s'intéresse ensuite à deux méthodes de preuves, en les validant (consistance et complétude) et en les implémentant. Après des rappels de logique élémentaire (logique propositionnelle et du premier ordre), le cours approchera les résultats fondamentaux de la logique qui mènent à la conception de deux paradigmes de programmation déclarative, la programmation fonctionnelle et la programmation logique. Le cours présentera : (1) le système de la déduction naturelle de Prawitz et le lambda-calcul de Curry. La notion de preuve comme fonction où programme -- ce qu'on appelle la correspondance de Curry-Howard -- sera illustrée. (2) le calcul de la résolution de Robinson, qui est le fondement pour la conception des démonstrateurs automatiques et des langages de programmation logique. Le cours soulignera les points communs entre ces deux paradigmes, par exemple l'algorithme d'unification, utilisé dans les algorithmes de typage des langages fonctionnels typés.

Plan :

Ressources pédagogiques fournies : Support de cours polycopiés, ouvrages, feuilles d'exercices.

Site Web  : http://www.lif.univ-mrs.fr/~lsantoca/teaching/LDP/

Apparaît dans les parcours