Brief on my thesis
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.