Michel Levy
Do you speak english ?
Adresse Professionnelle
D105 Bat D, Laboratoire LIG, 681 rue de la Passerelle
38400 SAINT MARTIN D'HERES
Téléphone : 04 76 82 72 46
Fax : 04 76 63 55 50
Par la traduction de Gödel, une formule A intuitionniste est traduite en
une formule modale B.
Par la méthode jointe, on sait
que A est valide intuitionnistiquement si et seulement si B est valide dans S4.
Si A est valide, le prouveur donne la preuve de B dans S4.
Si A n'est pas valide, le prouveur donne un contre-modèle de A
Enseignement
Recherche
- Démonstration automatique, utilisation d'assistants de preuve pour l'enseignement
-
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 prover9 , 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
Courriel : Michel.Levy[at]imag.fr
Dernière mise à jour : 04-May-2011