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