Projet Logique

Cette UE optionnelle de 6 ECTS se découpe en 15 séances de 1h30 pour un total de 22h30.
Ces séances ont lieu le lundi de 10h30 à 12h, en salle 1S53.
Plus d'informations ici.

Descriptif de l'UE

L'objectif de cette UE est de découvrir différents outils liés à la logique.
L'accent sera particulièrement mis sur l'assistant à la preuve Coq.

Modalités de validation

• DM
  • PARTIE 1 : La feuille donnée à la séance 3 à rendre sur eCampus pour le 13 mars 2023
  • PARTIE 2 - Sémantique :
    • Séances 8 et 9 : à rendre sur eCampus pour le 28 mars 2023
    • Séance 10 : à rendre sur eCampus pour le 5 avril 2023
• Projet
  • Lancement fin mars - début avril
• CC
  • Exercice LTac à commencer pour la séance 8 et à rendre sur eCampus pour le 17 mars 2022
  • Exercices Why3 de la séance 11 : à rendre sur eCampus pour le 30 avril 2023

Matériel pour les séances

• PARTIE A : Découverte de Coq
  • Séance 1 (16/01) - Prouver avec Coq : Feuille 1 (Corrigé), Feuille 2 (Corrigé) + Récapitulatif
  • Séance 2 (23/01) - Programmer avec Coq : Feuille 1 (Corrigé) + Récapitulatif
  • Séance 3 (30/01) - Séance d'exercices : Feuille 1
  • Séance 4 (06/02) - Séance d'exercices : Exercice 2 de la feuille précédente
  • Séance 5 (13/02) - Induction et Curry-Howard : Feuille Induction (Corrigé partiel), Feuille Curry-Howard + Récapitulatif
  • Séance 6 (20/02) - Extraction : Feuille 1
    • Vacances du 27/02 au 05/03
  • Séance 7 (06/03) - Induction en folie : Feuille 1
  • Travail pour la séance 8 : Tacticielle et Ltac : Feuille 1, Feuille 2
• PARTIE B : Sémantique
  • Séances 8 et 9 (13/03) - Introduction à K : Sujet de TP Matériel pour le TP
  • Séance 10 (20/03) (de 8h15 à 9h45) - Sémantique en Coq : Sujet de TP
• PARTIE C : Démonstration automatique
  • Séance 11 (27/03) - Introduction à Why3 :
    • Illustration avec l'exercice 1 (Division euclidienne) via https://why3.lri.fr/try/ + Slides
    • A faire : Exercice Dutch + Exercice Kadane + Complément sur les codes fantômes
  • Séance 12 (03/04) - Lancement du projet
    • Équipe Robinson - Sujet
    • Équipe Tab - Sujet
    • Équipe CC - Sujet
    • Équipe XelOR - Sujet
    • Équipe kHORN - Sujet
    • Équipe Coop - Sujet
    • Équipe Combo - Sujet
  • Matériel complémentaire :

Pentecôte 10/04

• Séance 13 (17/04) - Suite du projet
• Séance 14 (24/04) - Extension du projet

Vacances du 01/05 au 08/05

• Séance 15 (15/05) - Soutenance de projet

Contact

Pour toutes questions relatives à cette UE, merci de me contacter à l'adresse suivante : ledein (at) lsv (dot) fr