Preuves assistées par ordinateur
Cours de base (30 h de cours, 30h de TD)
Cours : Jean Duprat (Jean.Duprat)
TD : Florent Becker, Sylvain Chevillard (Florent.Becker, Sylvain.Chevillard)
L'objectif de ce module est de donner les notions de bases de la démonstration mathématique assistée par ordinateur. Il s'appuie largement sur le logiciel Coq mis au point par l'INRIA et disponible gratuitement. Ce module est susceptible d'intéresser trois publics différents : ceux qui souhaitent mener une réflexion sur ce qu'est la démonstration mathématique, la compréhension de ses aspects mécanisables apportant un éclairage novateur, ceux qui souhaitent être en mesure d'utiliser un logiciel d'assistance à la démonstration dans leurs travaux futurs, enfin ceux qui souhaitent poursuivre dans ce domaine de recherche qui est encore très ouvert.
Un plan rapide de ce cours est :
-
Expressions et types.
- Propositions et preuves.
- Logique et tactiques.
- Prédicats inductifs.
- Type de données inductive.
- Fonctions et spécifications.
- Récursion généralisée.
- Types co-inductifs (s'il reste du temps).
Bibliographie
Un seul livre couvre l'ensemble du programme : Interactive Theorem Proving and Program Development, Yves Bertot et Pierre Casteran, Springer. Le logiciel Coq et toute sa documentation est disponible sur le site de l'INRIA : http://coq.inria.fr/.