@INPROCEEDINGS{Schmidt06,
AUTHOR = {Schmidt, R. A.},
YEAR = {2006},
TITLE = {Developing Modal Tableaux and Resolution Methods via First-Order Resolution},
EDITOR = {Governatori, G. and Hodkinson, I. and Venema, Y.},
BOOKTITLE = {Advances in Modal Logic, Volume 6},
PUBLISHER = {College Publications},
ADDRESS = {London},
PAGES = {1--26},
NOTE = {Invited paper},
ISBN = {1-904987-20-6},
URL = {http://www.aiml.net/volumes/volume6/Schmidt.ps},
ABSTRACT = {
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.
}
}