Practical resolution of the coherence of formulas in modal logic • Valentin Montmirail
- Advisor :
- Daniel Le Berre
- Funding : Artois
- PhD defended on :
- Salle des thèses
In the past fifteen years, dramatic improvements in the context of testing propositional formulas consistency (SAT) have enabled a wide variety of satisfaction and optimization problems to be processed using a generic resolution engine: the SAT solver. Beyond SAT solvers, many fields using SAT world technics have benefited from these improvements: for example SAT modulo Theories (SMT) or Answer Set Programming (ASP). However, there are still many formalisms for which the coherence test does not pass the scale. This is the case for example when we add modal operators in a logical formula. The aim of this thesis is to design an effective resolution tool to test the consistency of logical formulas within modal logic, problems that we will 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 will be to design an “ad hoc” solver for Modal SAT adapting the principles and technics of the best solvers mentioned above. Checking 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 the thesis will be to collect and classify Modal SAT problems available in the community and create new ones.
Keywords: modal logics, benchmarks, automated reasoning