First-Order Resolution Methods for Modal Logics

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

In Podelski, A. and Voronkov, A. and Wilhelm, R. (eds), Volume in memoriam of Harald Ganzinger. Lecture Notes in Artificial Intelligence, Vol. ??? Springer. Invited overview paper, to appear. BiBTeX, PDF.

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.


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

Last modified: 24 Jan 13
Copyright © 2005-6 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk