R. A. Schmidt and U. Hustadt (2013): ``First-Order Resolution Methods for Modal Logics.'' In A. Voronkov and C. Weidenbach, editors, Programming Logics, pp. 345-391. Lecture Notes in Computer Science 7797, Springer.
Abstract, BibTeX, PDF (Springer).

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. [an error occurred while processing this directive]