LC - Logique classique

2026 - 2027

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 permier ordre

• [LC-TD.pdf]

• [LC-TP.pdf]

  • TP1 mardi 29/09/26 [lc_tp1.v]
  • TP2 lundi 07/10/26 [lc_tp2.v]
  • TP3 lundi 21/10/26 [lc_tp3.v]
  • TP4 lundi 18/11/26 [lc_tp4.v]

Instructions pour les TP

Sur les machines des salles de TP

On travaille sous Linux / Fedora avec RocqIDE.

Si Linux ou RocqIDE n’est pas disponible, vous pouvez utiliser JsCoq depuis n’importe quel navigateur / OS - Collez simplement le sujet du TP dans le cadre de gauche.

Sur votre machine personnelle

Travaillez de préférence avec RocqIDE, disponible sous tous les OS.

Linux / MacOS

Installez opam depuis les paquets, par exemple sous Ubuntu

sudo apt install opam

ou MacOS avec Homebrew

brew install opam

puis installez RocqIDE avec opam

opam install rocq-core rocqide

Windows / MacOS (alternative)

Installez Rocq Prover, voir la page https://rocq-prover.org/install.

Sous MacOS l’appli ouvre directement RocqIDE.

Tous OS (alternative)

Il est possible d’utiliser Rocq avec VSCode.

Commencez pour cela par installer le serveur de langage VsRocq, par exemple sous Linux / MacOS

opam install vsrocq-language-server

puis l’extension VsRocq dans VSCode.

ATTENTION actuellement vsrocq-language-server ne fonctionne pas avec OCaml 5.5 (voir l’issue). Si vous avez une version de OCaml >= 5.5, faites un switch opam vers OCaml 4.14.2 par exemple.

opam switch create 4.14.2
eval $(opam env)

puis

opam install rocq-core vsrocq-language-server

Si vous voulez revenir à votre installation précédente de OCaml :

opam switch default
eval $(opam env)

Pour faire du Ocaml (langages formels …)

Sur la page de Programmation fonctionnelle en L2, suivre les instructions.

Equipe pédagogique

• Sylvain Brandel (CM, TD et TP groupe A)
• Emmanuel Coquery (TD et TP groupe B)
• Damien Blanchard (TD et TP groupe C)
• Xavier Urbain (TD et TP groupe D)
• Paolo Pistone (TD groupe E)
• Samy Avrillon (TP groupe E)