@inbook {416,
	title = {Modal Satisfiability via {SMT} Solving},
	booktitle = {Software, Services, and Systems},
	series = {Lecture Notes in Computer Science},
	volume = {8950},
	year = {2015},
	pages = {30-45},
	publisher = {Springer International Publishing},
	organization = {Springer International Publishing},
	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.},
	isbn = {978-3-319-15544-9},
	doi = {10.1007/978-3-319-15545-6_5},
	url = {http://dx.doi.org/10.1007/978-3-319-15545-6_5},
	author = {Carlos Areces and Pascal Fontaine and Stephan Merz},
	editor = {De Nicola, R. and Hennicker, R.}
}