Outils pour utilisateurs

Outils du site


enseignement:masters:resume_preuves

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 succinte: - 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.

enseignement/masters/resume_preuves.txt · Dernière modification: 24/10/19 13:29 par Zielonka