Using resolution for testing modal satisfiability and building models

This paper presents a translation-based resolution decision procedure for the multimodal logic K(m) (∩, ∪, up curve sign) 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 that 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 as 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.