Michel Levy
Do you speak english ?
Je suis retraité depuis février 2010
Depuis cette date,
je suis collaborateur bénévole de l'université Joseph Fourier,
rattaché au laboratoire LIG.
On peut me joindre par courriel (voir ci-dessous)
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
Bijection entre les topologies d'Alexandroff et les préordres
Dans le document joint on définit une correspondance entre les
topologies d'Alexandroff sur un ensemble et les préordres sur cet ensemble et on prouve que cette
correspondance est une bijection.
Sémantique de Kripke et de Tarski pour la logique intuitionniste
Le document joint présente deux sémantiques
de la logique intuitionniste et prouve leur équivalence. La sémantique de Kripke
est basée sur un préordre, celle de Tarski sur la topologie d'Alexandroff
et le document montre comment associer ces deux sémantiques.
Explication de la méthode de D.W.Loveland
En démonstration automatique, la méthode, appelée en anglais "Model Elimination", est une méthode pour construire
des preuves en logique du premier ordre initialement présentée par
D.W.Loveland.
Cette méthode a été, depuis 1967, date de sa création, très utilisée mais mal expliquée.
Dans le document comprendre la Model Elimination ,
je m'efforce de donner cette explication, en prouvant la correction et la complétude de la méthode,
grâce à une séparation claire des cas propositionnel et du premier ordre et, dans le cas propositionnel,
en montrant pourquoi
les lemmes produits sont corrects.
Enseignement
Messieurs Pascal Lafourcade ,
Stéphane Devismes ,
et moi-même,
nous
avons écrit un livre pour enseigner la logique aux
étudiants de la licence de sciences :
Logique et démonstration automatique
Recherche
Démonstration automatique, utilisation d'assistants de preuve pour l'enseignement
- Logique modale non publié (ps)
- Ma thèse
déjà vieille
mais courte et intéressante
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.
Je rends hommage à William McCune
auteur du logiciel
prover9, remarquable logicien décédé prématurement en mai 2011.
Mais mon prouveur est é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 : 17-Apr-2016