LILaC
Coopération de démonstrateurs automatiques
pour les logiques modales
Situation du sujet
L'étude des
logiques modales
et en particulier celle des procédures de démonstration automatique
est une préoccupation majeure de l'équipe LILaC.
Ce stage sera dédié à deux types de méthodes, à savoir
SAT
et
les tableaux sémantiques.
-
La méthode des tableaux sémantiques est très populaire en logique modale.
Tandis que tous les démonstrateurs de la littérature ne
concernent que des familles de logiques très restreintes,
le démonstrateur automatique
Lotrec
developpe dans l'equipe se veut un outil générique.
Lotrec a aussi ete concu pour etre facilement interfacable
avec d'autres demonstrateurs, que ce soit des démonstrateurs
par tableaux ou non,
bien que cette possibilité n'ait pas été exploitée pour l'instant.
-
La méthode SAT étant actuellement la méthode la plus utilisée
pour la logique classique propositionnelle,
elle n'a pratiquement pas été appliquée aux logiques modales,
la seule exception étant les systèmes
Ksat et *SAT,
qui font coopérer SAT avec la methode des tableaux sémantiques.
Cependant, ces systemes sont pour l'instant restreints a des
logiques modales relativement simples.
Sujet
Comment les démonstrateurs par tableaux peuvent tirer profit
des progres dans le domaine SAT ?
En particulier, est-ce que la généricité de Lotrec peut etre combinée avec
la solution proposée dans *SAT ?
Pour pouvoir repondre a ces questions, nous proposons au stagiaire
la demarche suivante :
- bien assimiler la méthode des tableaux et le démonstrateur Lotrec
- se familiariser avec la méthode SAT
- étudier la solution proposée dans Ksat et *SAT,
et éventuellement proposer une alternative
- implanter *SAT (ou une alternative) dans Lotrec,
et faire des tests avec des logiques standards
Ce sujet de DEA doit évoluer vers un sujet de thèse,
qui pourrait aboutir a
-
une nouvelle proposition de combinaison de tableaux et SAT, voire
-
une étude générale des stratégies dans les démonstrateurs par tableaux
Profil recherché
- compétences en logique indispensables
(en particulier, intérêt pour la démonstration automatique)
- connaissance de Java
Encadrement scientifique et renseignements
le sujet sera encadré par
http://www.irit.fr/~Andreas.Herzig