Modal Satisfiability via SMT Solving

Carlos Areces, Pascal Fontaine, and Stephan Merz
Abstract
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.
© Springer 2015
Available as: PDF
Reference
@InCollection{areces:modal-smt,
  author =       {Carlos Areces and Pascal Fontaine and Stephan Merz},
  title =        {Modal Satisfiability via {SMT} Solving},
  booktitle =    {Software, Services, and Systems. Essays Dedicated to Martin
  Wirsing on the Occasion of His Retirement from the Chair of Programming and
  Software Engineering},
  publisher = {Springer},
  year =      2015,
  editor =    {Rolf Hennicker and Rocco {de Nicola}},
  volume =    8950,
  series =    {LNCS},
  pages =     {30-45},
}

Stephan Merz