LifLC - Logique classique

ANNEE 2024 - 2025

Planning global

Ressources pédagogiques

CM

• [LC-CM1.pdf] Partie 1 - Intro, rappels, inductifs …
• [LC-CM2.pdf] Partie 2 - Logique propositionnelle (mis à jour du 16/10/24)
• [LC-CM3.pdf] Partie 3 - Logique du premier ordre (mise à jour du 12/11/24)

TD

• [LC-TD1.pdf] Partie 1 - Rappels math, inductifs
• [LC-TD2.pdf] Partie 2 - Logique propositionnelle (avec résolution)
• [LC-TD3.pdf] Partie 3 - Logique du premier ordre

TP

• [LC-TP1.pdf] [lc_tp1.v]
• [LC-TP2.pdf] [lc_tp2.v]
• [LC-TP3.pdf] [lc_tp3.v]

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

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/coq/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/coq/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

Responsables

• LC - Logie classique : Sylvain Brandel
• LF - Langages formels : Xavier Urbain, page pédagogique de logique classique

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 30 septembre 2024
  • 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)
• Fabien De Marchi (TD et TP groupe C)
• Xavier Urbain (TD et TP groupe D)
• Mohand-Said Hacid (TD groupe E)
• Paolo Pistone (TD groupe F et TP groupe E)
• Joachim Cendrier (TP groupe F1)

Evaluation

• Contrôle continu intégral :
  • TP noté lundi 2 décembre 2024 8h ou 9h45
  • ECA mardi 17 décembre 2024 14h
  • Interros en début de TD, peut-être un autre TP noté …
  • Rattrapage en juin 2025
• Règles d’absences aux contrôles de TD :
  • Zéro en cas d’absence à un contrôle de TD, justifiée ou non, quelle qu’en soit la raison
  • Pas de rattrapage des contrôles en cas d’absence (légère tolérence au retard)
  • La moyenne des n contrôles sera calculée à partir des (n-1) meilleures notes
  • Le jury d’UE discutera des cas particuliers (absence longue durée, absences répétées …)