Cours

Polycopié (non mis à jour récemment!)

Diapos du cours 1 (12 septembre 2019)

Diapos du cours 2 (3 octobre 2019)

Diapos du cours 3 (22 novembre 2019), ainsi que le fichier coq utilisé pour la démo.

Exercices

Feuille d'exercices sur la logique minimale.

Feuille d'exercices sur la logique minimale avec négation et contradiction

Feuille d'exercices sur la logique propositionnelle

Feuille d'exercices sur la logique du premier ordre (modélisation)

Feuille d'exercices (preuves en logique du premier ordre)

Travaux dirigés sur machine

TDM 1: Premiers pas avec l'assistant de preuve Coq. Fichier minimale.v (logique minimale pure); fichier negation.v (logique minimale avec négation). Il s'agit de fichiers Coq: ils peuvent être ouverts avec le logiciel coqide, ou directement avec Emacs qui devrait lancer l'interface ProofGeneral.

TDM 2: Logique propositionnelle en Coq. Fichier Logique_prop.v. Les exercices proposés sont soit en commentaires, soit sous forme de preuves à compléter.

TDM 3: Logique du premier ordre. Fichier TM3.v

TP noté des 9 et 10 décembre

Les groupes A3, A5 et Maths-Info (y compris CMI) font leur TP noté lundi 9 décembre, 15h30.

Les groupes A1, A2 et A4 font leur TP noté mardi 10 décembre, 11h.

Répartition dans les salles du CREMI: pour le TP noté, la répartition des étudiants dans les différentes salles du CREMI est donnée dans les deux fichiers Lundi et Mardi. Si votre nom n'apparaît pas dans l'un des fichiers, vérifiez l'autre; les listes ont été établies sur la base des inscriptions officielles dans les groupes de TD. Merci de respecter cette répartition.

Liens (potentiellement) utiles

Vidéo: une série de vidéos sur la notion de démonstration, sur la chaîne YouTube "Monsieur Phi" (à la base c'est de la philosophie, et c'est très bien fait; il y a une demie-douzaine d'épisodes sur la démonstration)

Les documents proposés ici partent d'un niveau très élémentaire, mais vont tous bien au-delà de ce qui est proposé dans le cours.

Le site de Pierre Castéran consacré à son livre Le Coq'Art (version française librement téléchargeable)

Un tutoriel sur Coq

Petit guide de survie en Coq: un aide-mémoire sur les commandes Coq les plus fréquentes. Attention, le vocabulaire utilisé n'est pas exactement le même qu'en cours (mais les exemples Coq devraient aider quand même).

QED, un environnement interactif d'exercices à la formulation de preuves formelles en logique propositionnelle.

Annales

Sujets de 2018-19 session 1, session 2.

Sujets de 2017-18 session 1, session 2.

Sujets de 2016-17 session 1, session 2.

Un exemple de sujet de TP noté (2017). L'exercice consistait à remplacer les preuves omises ("Admitted") par des scripts de preuves corrects. Une solution (sans commentaires ni explications) est disponible, mais il est fortement conseillé de résoudre les exercices sans la consulter.