===== Preuves Assistées par Ordinateur (Master 1) =====

**Ce cours est maintenant assuré par Hugo Herbelin. Les documents ci-dessous concernent l'ancienne version du cours**

Notes de cours (préparées par Alexandre Miquel):
  * Le [[http://www.irif.fr/~letouzey/preuves/cours.pdf|document principal]]
  * Le [[http://www.irif.fr/~letouzey/preuves/cours_lam.pdf|système T de Gödel]]
  * Un [[http://www.irif.fr/~letouzey/preuves/guide.html|petit guide de survie]] pour Coq

Quelques notes pour le [[https://gitlab.math.univ-paris-diderot.fr/letouzey/cours-preuves/blob/master/cours1.md|cours 1]].

L'encodage Coq de la déduction naturelle présenté en cours : [[https://gitlab.math.univ-paris-diderot.fr/letouzey/natded|NatDed]].

Annales d'examen : [[http://www.irif.fr/~letouzey/preuves/exam-2015.pdf|sujet de mai 2015]].

Projet 2019-2020 : le [[https://gaufre.informatique.univ-paris-diderot.fr/letouzey/projet-preuves-2020|dépot git]] à forker. Plus d'information dans le [[https://gaufre.informatique.univ-paris-diderot.fr/letouzey/projet-preuves-2020/blob/master/README.md|README]].

Sujets des TD/TP:
  * TD1 (déduction naturelle): [[http://www.irif.fr/~letouzey/preuves/td1.pdf|pdf]]
  * TD2 (premiers pas en Coq): [[https://gitlab.math.univ-paris-diderot.fr/letouzey/cours-preuves/blob/master/td2.md|markdown]]
  * TD3 (arithmétique de Peano): [[http://www.irif.fr/~letouzey/preuves/td3.pdf|pdf]]
  * TD4 (maths élémentaires en Coq): [[https://gitlab.math.univ-paris-diderot.fr/letouzey/cours-preuves/blob/master/td4.md|markdown]]
  * TD5 (entiers naturels en Coq): [[https://gitlab.math.univ-paris-diderot.fr/letouzey/cours-preuves/blob/master/td5.md|markdown]]
  * TD6 (listes en Coq): [[https://gitlab.math.univ-paris-diderot.fr/letouzey/cours-preuves/blob/master/td6.md|markdown]]
  * TD7 (théories et modèles): [[http://www.irif.fr/~letouzey/preuves/td7.pdf|pdf]]
  * TD8 (prédicats inductifs): [[https://gitlab.math.univ-paris-diderot.fr/letouzey/cours-preuves/blob/master/td8.md|markdown]]
  * TD9 (énigme de MU): [[https://gitlab.math.univ-paris-diderot.fr/letouzey/cours-preuves/blob/master/td9.md|markdown]]
  * TD9bis (damier): [[https://gitlab.math.univ-paris-diderot.fr/letouzey/cours-preuves/blob/master/td9bis.md|markdown]]
  * TD10 (système T et théorie des types simples): [[http://www.irif.fr/~letouzey/preuves/td10.pdf|pdf]]