Bilal Said - LoTREC: déduction automatique par tableau en logique modale à la toulousaine

Dans cet exposé, je vous parlerai du problème de satisfiabilité en logique modale, et je vous présenterai LoTREC: un outil qui permet l'implémentation d'une procédure automatique de résolution de ce problème.

Grâce à un langage simple et de haut niveau, on peut créer sa propre méthode de tableau, sans avoir besoin d'aucune expertise spécifique en programmation. Ensuite, on peut expérimenter avec des formules en visualisant et analysant les modèles (et/ou contre-modèles) générés par LoTREC. On peut faire du model checking, démarrer avec des modèles partiels et intervenir durant l'exécution si sa procédure est semi-automatique.

Je vous parlerai également des bases théoriques qui permettent de certifier les algorithmes obtenus en tant que terminant et corrects. Après une démonstration du logiciel, je terminerai par la discussion des perspectives du développement de cette plateforme.