Recently lot of work has been done considering satisfiability of formulas in specific theory (array theory, bit-vector theory). But I did not find any results about satisfiability modulo theory in the context of modal logic ? Is there any reasons ? Is it useful to consider modal logic and satisfiability modulo theory ??
Thanks.
we have been working on SMT for modal logics, and we managed to prove that SMT with quantification yields a decision procedure for the basic modal logic (BML). This is not hard to prove when you work with the standard translation of the BML and common instanciation rules available in some SMT solvers. We also have the same results for other operators (inverse operator, graded operator). Ultimately our goal is to prove that SMT yields a decision procedure for the entire guarded fragment, which we guess that it is the case, but so far we didn't came up with satisfactory proof. In terms of efficiency, we are currently running some tests to see how an SMT prover does with modal formulas. So far, I don't have the numbers.