• Thèse soutenue le :
  • 2018-09-17
  • Salle des thèses

Ces quinze dernières années, des progrès spectaculaires dans le cadre du test de cohérence de formules propositionnelles (SAT) ont permis à une grande variété de problèmes de satisfaction et d’optimisation d’être traités à l’aide d’un moteur de résolution générique, le solveur SAT. Au delà des seuls solveurs SAT, de nombreux cadres utilisant des techniques issues du monde SAT ont pu bénéficier de ces améliorations : on citera par exemple SAT modulo Theories (SMT) ou Answer Set Programming (ASP). Cependant, il existe encore de nombreux formalismes pour lesquels le test de cohérence ne passe pas à l’échelle. C’est le cas par exemple dès que l’on rajoute des opérateurs modaux dans une formule logique. Le but de cette thèse est de concevoir un outil de résolution efficace pour tester la cohérence de formules logiques dans le cadre de la logique modale, problème que nous appellerons Modal SAT. Une première approche sera d’étudier les diverses façons de réduire le problème Modal SAT à un problème pour lequel il existe des solveurs efficaces en pratique : par exemple SAT, SMT ou ASP. Une autre approche sera de concevoir un solveur “ad hoc” pour Modal SAT en adaptant les principes et techniques des meilleurs solveurs cités plus haut. L’évaluation de solveurs requiert un ensemble varié de benchmarks, idéalement représentant des problèmes Modal SAT réels (par opposition aux problèmes générés aléatoirement ou aux exemples académiques). Un aspect important de la thèse sera de collecter et classer les problèmes Modal SAT disponibles dans la communauté et d’en créer de nouveaux.

Mots-clés: logiques modales, évaluation, raisonnement automatique