Affordable Access

First-Order Resolution Methods for Modal Logics

Publication Date
  • Logic
  • Mathematics


In this paper we give an overview of results for modal logic whichcan be shown using techniques and methods from first-order logicand resolution.Because of the breadth of the area and the many applications wefocus 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 oftranslating modal logics into first-order logic, we exploredifferent ways of using first-order resolution theorem provers tosolve a range of reasoning problems for modal logics,and we discuss a variety of results which have been obtainedin the setting of first-order resolution.

There are no comments yet on this publication. Be the first to share your thoughts.