Différences

Ci-dessous, les différences entre deux révisions de la page.

--- formations:masters:cours:resume_preuves [2021/02/03 17:36] – ↷ Page déplacée de formations:masters:1ere_annee:cours:resume_preuves à formations:masters:cours:resume_preuves admin
+++ formations:masters:cours:resume_preuves [2022/07/26 19:04] (Version actuelle) – modification externe 127.0.0.1
@@ Ligne 1: / Ligne 1: @@
+====== 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.