First-Order Resolution Methods for Modal Logics

Schmidt, R. A. and Hustadt, U. (2013)

In Voronkov, A. and Weidenbach, C. (eds), Programming Logics: Essays in Memory of Harald Ganzinger. Lecture Notes in Computer Science 7797, Springer, 345-391. Invited overview paper. BiBTeX, DOI.

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.

Version of 2006.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 17 Jun 13
Copyright © 2006-13 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk