I'm PHD Student in Artificial Intelligence @CRIL (Centre de Recherche en Informatique de Lens).

The aim of my thesis is to design an effective resolution tool to test the consistency of logical formulas in modal logic problem that we call Modal-SAT. One approach is to study the various ways to reduce the problem to a SAT problem for which there are effective solvers in practice: for example SAT, SMT or ASP. Another approach is to design a solver "ad hoc" for Modal-SAT adapting the principles and techniques of the best solvers mentioned above.

The evaluation of solvers requires a diverse set of benchmarks, ideally representing actual Modal-SAT problems (as opposed to randomly generated problems or academic examples). An important aspect of my thesis will be to collect and classify Modal SAT problems available in the community and create new ones.

In particular, the thesis will focus on games with epistemic modeling aspects, ie games (cooperative or not) where the participants must reason on the knowledge that the other participants have of the game. The result of the thesis should ideally be the realization of a software player capable of participating in this type of game, using the Modal-SAT solver as the only reasoning engine.