2015 | OriginalPaper | Buchkapitel
Modal Satisfiability via SMT Solving
Autoren: Carlos Areces, Pascal Fontaine, Stephan Merz
Verlag: Springer International Publishing
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.
