Modal logics extend classical propositional logic, and they are robustly decidable. Whereas most existing decision procedures for modal logics are based on tableau constructions, we propose a framework for obtaining decision procedures by adding instantiation rules to standard SAT and SMT solvers. Soundness, completeness, and termination of the procedures can be proved in a uniform and elementary way for the basic modal logic and some extensions.
CITATION STYLE
Areces, C., Fontaine, P., & Merz, S. (2015). Modal satisfiability via SMT solving. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8950, 30–45. https://doi.org/10.1007/978-3-319-15545-6_5
Mendeley helps you to discover research relevant for your work.