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},
}