@ARTICLE{HustadtSchmidt02a,
AUTHOR = {Hustadt, U. and Schmidt, R. A.},
MONTH = feb,
YEAR = {2002},
TITLE = {Using Resolution for Testing Modal Satisfiability and Building Models},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {28},
NUMBER = {2},
PAGES = {205--232},
ISBN = {0168-7433},
ABSTRACT = {This paper presents a translation-based resolution decision
procedure for the multi-modal logic $\textit{K}_{(m)}(\cap,\cup,\smile)$
defined over families of relations closed under intersection, union and
converse.  The relations may satisfy certain additional frame
properties.  Different from previous resolution decision procedures
which are based on ordering refinements our procedure is based on a
selection refinement, the derivations of which correspond to derivations
of tableaux or sequent proof systems.  This procedure has the advantage
that it can be used both as a satisfiability checker and a model
builder.  We show that tableaux and sequent-style proof systems can be
polynomially simulated with our procedure.  Furthermore, the finite
model property follows for a number of extended modal logics.},
}