bookPart
Modal satisfiability via SMT solving
Fecha
2015Autor
Areces, Carlos Eduardo
Fontaine, Pascal
Merz, Stephan
Institución
Resumen
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.