@INCOLLECTION{SchmidtHustadt06a,
AUTHOR = {Schmidt, R. A. and Hustadt, U.},
YEAR = {2006},
TITLE = {First-Order Resolution Methods for Modal Logics},
EDITOR = {Podelski, A. and Voronkov, A. and Wilhelm, R.},
BOOKTITLE = {Volume in memoriam of {H}arald {G}anzinger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {??},
PUBLISHER = {Springer},
NOTE = {Invited overview paper, to appear},
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 which are
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,
and we discuss a variety of results which have been obtained
in the setting of first-order resolution.
}
}