Ce cours s'articule en deux parties :
a) apprentissage du langage Caml (un dialecte de ML)
b) implantation d'algorithmes de demonstration automatique.
a) Le langage ML est essentiellement base sur le formalisme du lambda-calcul etendu par des types de donnees recursifs tels les listes, les arbres etc... Il a ete originellement concu pour faciliter l'implantation de formalismes logiques ce qui en fait l'interet pour nous. Le dialecte Caml que nous etudierons a su integrer harmonieusement au langage originel des traits usuels et fort utiles de programmation tels un mecanisme d'exception, la gestion de donnees mutables, un systeme de modules, ce qui facilite le developpement de programmes en taille reelle.
b) Les algorithmes de demonstration automatique jouent un role de premiere importance dans certains domaines d'intelligence artificielle ainsi que dans celui du developpement d'outils d'aide a la demonstrations. Ces derniers sont des elements centraux pour la mise en oeuvre des systemes de specification et certification du logiciel. Nous etudierons trois classes d'algorithmes : decison du calcul propositionnel, methodes de resolution pour le calcul des predicats du premier ordre et methodes de preuves inductives basees sur la reecriture.
L'objectif de ce cours de fournir aux etudiants une bonne maitrise pratique d'une application importante de la logique au monde informatique.