Cours de Logique

Pour travailler sous Proof General

Ajouter à votre fichier de configuration .emacs ou .xemacs/init.el la ligne suivante:
 (load "/usr/share/emacs/site-lisp/proofgeneral/generic/proof-site.el")

ou bien
M-x proofgeneral

C-x C-f votre_fichier.v

Exercices (à télécharger)

  1. Logique minimale propositionnelle
  2. Une solution
  3. Logique propositionnelle
  4. Une solution
  5. Une autre solution
  6. Une théorie du premier ordre : relation d'ordre total non bornée
  7. Une théorie du premier ordre : relation d'ordre total non bornée (Corrigé)
  8. Une théorie du premier ordre : relation d'ordre total non bornée (Corrigé sans auto)
  9. Quelques tautologies en logique du premier ordre
  10. Le Paradoxe du barbier
  11. Un peu de second ordre
  12. Prouver les deux derniers lemmes du développement sur Peano

Exemples

  1. Pour les impatients : un avant goût de la logique du premier ordre
  2. L'argument diagonal de Cantor
  3. Arithmétique de Peano

Projet 08-09

Le projet consiste à remplacer le plus possible d'Admitted par des vraies preuves dans ce développement
Le barème est volontairement "libéral".
Il y a 30 Admitted à traiter, on compte 0.6 point par preuve complétée, avec un maximum de 12 points (obtenables avec 20 preuves finies).
Un petit rapport est demandé (6 à 8 pages) décrivant les étapes principales des raisonnements qui vous ont demandé de la réflexion, les outils que vous avez élaborés ou appris à utiliser, etc.
Vous devrez envoyer un fichier .v comportant vos preuves; votre rapport ne sera donc pas une copie des listings de vos preuves!
Ce rapport sera évalué sur 8 points.


Ce projet est à faire par binôme (à l'intérieur d'un même groupe de TD )
Date de remise : Vendredi 31 Octobre à 23h59, sous forme d'une archive de type tar.gz contenant votre solution et le rapport (en pdf). Afin d'éviter toute confusion, votre archive devra contenir un répertoire dont le nom est composé des noms des participants du binôme.


Toute question sur ce projet peut être adressée aux trois enseignants: (Frédérique Carrère, Pierre Castéran et Laurent Méhats), avec "projet Coq" dans le sujet du courrier. Les réponses seront publiées dans une FAQ .

Une proposition de corrige

Préparation à l'examen de Décembre 2008

Quelques informations et conseils
Un fichier Coq sur lequel travailler

Documentation