@Article{Areces2001i,
  author =       "C. Areces and H. de Nivelle and M. de Rijke",
  journal =      "Journal of Logic and Computation",
  title =        "Resolution in Modal, Description and Hybrid Logic",
  year =         "2001",
  number =       "5",
  abstract =     "We provide a resolution-based proof procedure for
                 modal, description and hybrid logic that improves on
                 previous proposals in important ways. It avoids
                 translations into large unde- cidable logics, and works
                 directly on modal, description or hybrid logic formulas
                 instead. In addition, by using the hybrid machinery it
                 avoids the complexities of earlier propositional
                 resolution-based methods for modal logic. It combines
                 ideas from the method of prefixes used in tableaux, and
                 resolution ideas in such a way that some of the
                 heuristics and optimizations devised in either field
                 are applicable.",
  pages =        "717--736",
  volume =       "11",
                 Description Logics",
}