@INCOLLECTION{SchmidtHustadt13,
AUTHOR = {Schmidt, R. A. and Hustadt, U.},
YEAR = {2013},
TITLE = {First-Order Resolution Methods for Modal Logics},
EDITOR = {Voronkov, A. and Weidenbach, C.},
BOOKTITLE = {Programming Logics: Essays in Memory of {H}arald {G}anzinger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {7797},
PUBLISHER = {Springer},
PAGES = {345--391},
NOTE = {Invited overview paper},
DOI = {http://dx.doi.org/10.1007/978-3-642-37651-1_15},
ABSTRACT = {
In this paper we give an overview of results for modal logic which
can be shown using techniques and methods from first-order logic
and resolution.
Because of the breadth of the area and the many applications we
focus on the use of first-order resolution methods for modal logics.
In addition to traditional propositional modal logics we 
consider more expressive \PDL-like dynamic modal logics 
closely related to description logics.
Without going into too much detail, we survey different ways of
translating modal logics into first-order logic, we explore
different ways of using first-order resolution theorem provers to
solve a range of reasoning problems for modal logics,
and we discuss a variety of results which have been obtained
in the setting of first-order resolution.
}
}