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.

• 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, …)

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

• 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, Interactive Theorem Proving and Program Development. Coq'Art : The Calculus of Inductive Constructions. Springer Verlag, 2004.