@INCOLLECTION{HustadtSchmidt00c,
AUTHOR = {Hustadt, U. and Schmidt, R. A.},
YEAR = {2000},
TITLE = {Using Resolution for Testing Modal Satisfiability and Building Models},
EDITOR = {Gent, I. P. and van Maaren, H. and Walsh, T.},
BOOKTITLE = {SAT 2000: Highlights of Satisfiability Research in the Year 2000},
SERIES = {Frontiers in Artificial Intelligence and Applications},
VOLUME = {63},
PUBLISHER = {IOS Press},
ADDRESS = {Amsterdam},
NOTE = {Also to appear in a special issue of \emph{Journal of Automated Reasoning}},
ISBN = {1 58603 061 2},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/HustadtSchmidt00c.html},
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.}
}