LC - Logique classique

2025 - 2026

Planning global

Ressources pédagogiques

• [LC-CM1.pdf] Partie 1 - Intro, rappels, inductifs
• [LC-CM2.pdf] Partie 2 - Logique propositionnelle

• [LC-TD.pdf]

• [LC-TP.pdf]
  • TP1 mardi 30/09/25 [lc_tp1.v]
  • TP2 lundi 13/10/25
  • TP3 lundi 03/11/25
  • TP4 lundi 24/11/25

Instructions pour les TP

• On utilise Coq depuis une IDE (CoqIDE, VSCode, EMACS …)

• Lancez votre IDE :

  • CoqIDE, disponible sur les machines des salles de TP du campus (Linux uniquement)
  • VSCode, disponible sur les machines des salles de TP du campus, nécessite d’installer l’extension VsCoq avec la version 0.3.9
  • EMACS avec Proof General …

• Téléchargez le fichier .v (lien ci-dessus), ouvrez-le dans votre IDE, lisez le sujet et complétez le fichier.v dans votre IDE

Alternative à une IDE : JsCoq ; Collez le sujet du TP dans le cadre de gauche (non recommandé, l’usage est peu convivial)

Pour voir correctement le sujet dans votre navigateur, configurez l’encodage par défaut de votre navigateur en Unicode (UTF-8)

Pour travailler sur votre machine personnelle

Pour installer CoqIDE sur votre machine

Les installeurs de CoqIDE incluent Coq

• MacOS :

  • Installeur binaire sur https://github.com/rocq-prover/platform/releases/latest (inclut CoqIDE)
  • Avec Homebrew : brew install coqide

• Windows : plusieurs manières d’installer CoqIDE, cf. Installer Coq sous Windows :

  • Installeur binaire sur https://github.com/rocq-prover/platform/releases/latest (inclut CoqIDE)
  • Installer Linux dans une VM ou dans WSL puis suivre les instructions pour Linux

• Linux : cf. Installer Coq sous Linux (de préférence avec opam)

Pour utiliser Coq avec VSCode

• Installez Coq (cf. ci-dessus)
• Installez l’extension VsCoq dans VSCode, précisez version 0.3.9.

Organisation

Volume

• CM : 12 heures (8 x 1h30)
• TD : 12 heures (8 x 1h30)
• TP : 6 heures (4 x 1h30)

Horaires

• Tous les enseignements de LC (et LF) ont lieu dans la séquence 1 (lundi matin et mardi après-midi)
• Globalement, les CM ont lieu le mardi après-midi de 14h à 15h30, les TD / TP le lundi matin de 8h à 9h30 et de 9h45 à 11h15 ou de 11h30 à 13h ; chaque créneau de 8h à 9h30 et de 9h45 à 11h15 ou de 11h3à à 13h est occupé soit par un TD / TP de théorie des langages, soit par un TD / TP de logique classique
• À partir du 6 octobre 2025
  • TD de LC ou de LF de 8h à 9h30
  • TP de LC ou de LF de 9h45 à 11h15 ou de 11h30 à 13h
• Fiez-vous à votre emploi du temps sur ADE

Intervenants

• Sylvain Brandel (CM, TD et TP groupe A)
• Emmanuel Coquery (TD et TP groupe B)
• Damien Blanchard (TD et TP groupe C)
• Jey Puget-Gil (TD et TP groupe D)
• Paolo Pistone (TD groupe E)

Salles d’enseignement

• CM : Amphi 5 déambu
• TD et TP groupe A : Quai 43 s. 112
• TD et TP groupe B : Quai 43 s. 113
• TD et TP groupe C : Quai 43 s. 114
• TD et TP groupe D : Quai 43 s. 116
• TD groupe E : Grignard A
• TP groupe E : ventilé dans les salles du Quai 43 (cf. TOMUSS)

Evaluation

L’UE est en contrôle continu intégral, avec 3 épreuves :

• Une interrogation d'1h, en séance de TD le lundi matin, lundi 6 octobre 2025 à 8h00
• Un TP noté de 30 minutes lundi 1er décembre 2025, date à confirmer
• Une interrogation finale d'1h mardi 2 décembre 2025, date à confirmer

Outre ces 3 épreuves, il y aura une épreuve de seconde chance, la date sera précisée ultérieurement. Tout le monde pourra participer à cette épreuve, la note obtenue remplacera la moins bonne des 2 notes d’interrogation obtenues précédement, si elle est supérieure à celle-ci. Le TP noté ne pourra pas être remplacé par l’E2C.

Règles concernant les absences aux contrôles :

• Zéro à l’épreuve en cas d’absence, qu’elle soit justifiée ou non,
• En cas d’absence justifiée ou non à une épreuve, la note de l’E2C remplacera cette absence,
• En cas d’absences justifiées à deux épreuves ou plus, nous pourrons proposer des épreuves de substitutions, au cas par cas.