====== Preuves assistées par ordinateur ======

Introduction à la démonstration assistée par ordinateur, en vue de formaliser des mathématiques ou de certifier des logiciels.  Vérification de preuves, recherche automatique ou guidée par l'utilisateur.

==== Systèmes logiques étudiés ====

  * calcul des prédicats du 1er ordre (déduction naturelle) et sa méta-théorie
  * initiation à l'ordre supérieur (lambda-calcul typé, système T, ...)

==== Objectifs ====
  * Savoir faire une preuve en déduction naturelle.
  * Savoir exprimer un énoncé puis mener une preuve simple dans un outil tel que Coq.

==== Bibliographie succincte ====
  * R. David, K. Nour et C. Raffalli, Introduction à la logique : théorie de la démonstration, Dunod, Paris, 2001.
  * Y. Bertot et P. Castéran, [[http://www.labri.fr/perso/casteran/CoqArt|Interactive Theorem Proving and Program Development. Coq'Art : The Calculus of Inductive Constructions.]] Springer Verlag, 2004.