Resolution in Modal, Description and Hybrid Logic

C. Areces, H. de Nivelle, and M. de Rijke. Resolution in Modal, Description and Hybrid Logic. Journal of Logic and Computation, 11(5):717–736, 2001.

Download

[pdf] 

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.

BibTeX

@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",
}