Logique, réduction, résolution

Presente deux paradigmes de calcul sous l'angle de la logique : la reduction, base de la programmation logique, est etudiee a travers le lambda-calcul; pour la resolution, ce sont la validite, la completude voire l'equite du calcul qui importent. Les systemes d'inference et les methodes semantiques de la logique sont presentes et appliques a l'etude de ces proprietes, et des problemes d'effectivite. Deux langages recents fondes sur ces principes sont utilises : CAML et NU-Prolog. Chaque chapitre est suivi d'exercices, resolus pour certains