Logique J1IN7M21

Slides in pdf

  1. Introduction au cours

Coq Scripts

  1. Cours2.v : Propositional Logic
  2. Cours3.v : First Order Logic
  3. Introduction to inductive predicates : le
  4. More about lists

Coq quick reference sheet

Principales commandes

Le Coq'Art en V.F.

Download

La page d'Yves Bertot

Yves Bertot chercheur à l'INRIA, et co-auteur du Coq'Art, a écrit un nombre impressionnant de tutoriels sur Coq, et ses diverses applications en mathématiques et informatique. Cliquez donc ici !

TP noté Décembre 2014

Solution ici

Archives examens

Détails pratiques

Il y a deux outils pour travailler en Coq.
Pour les habitués d'Emacs : utiliser Proof General (voir note en bas de page), qui est un mode Emacs spécialisé dans les preuves interactives.

Ceux qui préfèrent les "ide" , utiliser coqide, l'environnement de développement intégré pour Coq.
coqide est moins usine à gaz qu'Eclipse. Si un bug provoqué par la diabolique touche MOD4 (celle avec une fenêtre tordue) de votre clavier se produit, alors éditer votre fichier $HOME/.coqiderc et remplacer toutes les occurrences de MOD4 par MOD1, puis relancer.

Liens et informations utiles