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.