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-CM3.pdf] Partie 3 - Logique du premier ordre

• [LC-TD.pdf]

• [LC-TP.pdf]
  • TP1 mardi 30/09/25 [lc_tp1.v]
  • TP2 lundi 13/10/25 [lc_tp2.v]
  • TP3 lundi 03/11/25 [lc_tp3.v]
  • 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
• Une interrogation finale d'1h lundi 1er décembre 2025 à 8h amphis Déambu 4 et 5,
• Un TP noté de 30 minutes mardi 2 décembre 2025 à partir de 14h Quai 43 s. 112, 113, 114 et 116.

Outre ces 3 épreuves, il y aura une épreuve de seconde chance (E2C) qui sera planifiée par la scolarité entre le 15 décembre 2025 et le 9 janvier 2026, la date exacte 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.
La note de TP noté ne pourra pas être remplacée par la note de 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.