Modal Satisfiability via SMT Solving

C. Areces, P. Fontaine, and S. Merz. Modal Satisfiability via SMT Solving. In R. De Nicola and R. Hennicker, editors, Software, Services, and Systems, Lecture Notes in Computer Science, pp. 30–45, Springer International Publishing, 2015.

Download

[pdf] 

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.

BibTeX

@InCollection{Areces2015c,
  author =       "C. Areces and P. Fontaine and S. Merz",
  booktitle =    "Software, Services, and Systems",
  publisher =    "Springer International Publishing",
  title =        "Modal Satisfiability via {SMT} Solving",
  year =         "2015",
  editor =       "R. De Nicola and R. Hennicker",
  ISBN =         "978-3-319-15544-9",
  pages =        "30--45",
  series =       "Lecture Notes in Computer Science",
  volume =       "8950",
  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.",
  doi =          "10.1007/978-3-319-15545-6_5",
  owner =        "areces",
  timestamp =    "2014.11.30",
  URL =          "http://dx.doi.org/10.1007/978-3-319-15545-6_5",
  ISBN =         "978-3-319-15544-9",
}