Ce cours est une introduction à la formalisation des mathématiques, en théorie et en pratique, et à la résolution de problèmes logiques à l'aide d'ordinateurs.
Il revient sur les fondements théoriques des mathématiques, sous la forme de la Théorie des Ensembles et de ses alternatives plus computer-friendly, et il parcourt les techniques très diverses de la Déduction Automatique à la preuve interactive de théorèmes.
Les TD utiliseront l'assistant à la preuve Coq, notamment pour la formalisation de problèmes d'algèbre et de leur preuves.
Mais des SAT-solveurs, des SMT-solveurs ou des prouveurs automatiques pourront être utilisés pour illustrer d'autres techniques et applications.
Les étudiants bénéficieront d'initiative et de flexibilité sous la forme de mini-projets, ou de moins-mini-projets pour ceux qui décident d'approfondir ces thèmes dans l'EA MAT/INF571.

COURS:

Formalisation des problèmes et des théories mathématiques

- Rappels :
logique, modèles, arithmétiques de Péano et de Presburger, théorèmes de Church et Goedel.
- Théorie des ensembles :
Version naïve et paradoxe de Russel, axiomes de Zermelo-Fraenkel, indécidabilité et incomplétude.
Ordinaux et récurrence transfinie, axiomes du choix et du continu.
- Théorie des fonctions :
Lambda-calcul et paradoxe de Russel, théorie des types.
- Preuves constructives :
contenu calculatoire des preuves, versions constructives du choix, fondements de Coq.

Méthodes de démonstration automatique

- Dans le cas de théories décidables : SAT et SAT-modulo-Theory.
- Dans certaines théories: élimination des quantificateurs.
- Recherche de preuve généraliste : preuve en avant / en arrière, unification.
- Recherche de preuve comme principe de programmation : introduction à la programmation logique / ProLog.


TD sur machine:

Introduction à la pratique de Coq, exercices d'arithmétique, etc...
Extraction de programme à partir d'une preuve constructive : exemple d'un programme de tri.
SAT : Programmation d'un SAT-solveur basique. En Coq-même ou dans un autre language.
Projet en Coq ou programmation d'un prouveur dans un langage au choix.

Niveau requis : INF431 n'est pas un pré-requis. INF423 est très conseillé, même s'il est possible d'acquérir rapidement les concepts nécessaires (formules logiques, modèles, preuves, fonctions calculables,...)

Modalités d'évaluation : Examen sur table (2 ou 3 heures), pour ceux qui prennent ce module comme cours. Mini-projet, pour ceux qui prennent ce module comme EA.

Dernière mise à jour : vendredi 22 mars 2013