Developing modal tableaux and resolution methods via first-order resolution

This paper explores the development of calculi using different proof methods for propositional dynamic modal logics. Dynamic modal logics are PDL-like extended modal logics which are closely related to description logics. We show how tableau systems, modal resolution systems and Rasiowa-Sikorski systems, which are dual tableau systems, can be developed and studied by using standard principles and methods of first-order theorem proving. We translate modal logic reasoning problems to first-order clausal form and then use a suitable refinement of resolution to construct and mimic derivations using the desired proof method. The inference rules of the calculus can then be read off from the clausal form used. © 2006, Renate A. Schmidt.