Modal Satisfiability via SMT Solving

Areces, C., Fontaine, P., and Merz, S.. Modal Satisfiability via SMT Solving. In De Nicola, R. and Hennicker, R., 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: (download)

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

Generated by bib2html.pl (written by Patrick Riley) on Sun Oct 02, 2016 17:05:49