Michel Levy

Adresse Professionnelle

Le coin de la déduction naturelle : assistants de preuve, cours et documents

Enseignement

• L3 informatique UE LSF
  
• année 2006
• L2 UE INF242
  
• année 2007
• Maitrise d'informatique niveau M1, c'est-à-dire Bac+4
  
• 2001 programmation fonctionnelle
  
introduction au lambda-calcul (ps,pdf)
• 2001 intelligence artificielle
présentation de PVS (ps,pdf)
• Licence L2, c'est-à-dire Bac+2
  
• 2002 UE MILPL logique et programmation logique 
• Programmation logique
• Logique
  
• Examen de mai 2002 (ps,pdf) et son corrigé (ps,pdf)

Recherche

•  A PVS-based approach for teaching Constructing Correct Iterations FM99 (ps)
• Même thème en français RFIA2002 (ps)
• Logique modale non publié (ps)

Logiciels

• Stratégie complète pour la résolution propositionnelle.
• Donnée : une liste de clauses, Résultat : une liste des clauses non valides conséquences minimales de la donnée

et les preuves de ces clauses.
Si l'on voit la donnée comme une somme de monômes, le résultat est la base complète des monômes premiers de la somme.
• Utilisation : charger le fichier ResPropSc.tar, le désarchiver (tar xvf ResPropSc.tar),

lire le fichier LISEZ-MOI du répertoire créé par la commande tar.


• Stratégie complète pour la résolution au premier ordre. Ce prouveur n'est pas bien rapide.  Avec otter, vous avez un prouveur bien meilleur. Mais mon prouveur est en écrit en Ocaml, vous avez le source et la trace des preuves est une mine d'exercices pour les étudiants et les enseignants. Pour l'exécuter il vous faut Ocaml, charger le fichier ResolutionPo.tar, le désarchiver, lire LISEZ-MOI.
  

Liens utiles

• Le site Ocaml  inria

Courriel : Michel.Levy[at]imag.fr

Dernière mise à jour :  24 octobre 2006