Prefixed resolution: a resolution method for modal and description logics

C. Areces, H. de Nivelle, and M. de Rijke. Prefixed resolution: a resolution method for modal and description logics. In Automated deduction --- CADE-16 (Trento, 1999), pp. 187–201, Springer, Berlin, Germany, 1999.

Download

[pdf] 

Abstract

We provide a resolution-based proof procedure for modal and description logics that improves on previous proposals in a number of important ways. First, it avoids translations into large undecidable log- ics, and works directly on modal or description logic formulas instead. Second, by using labeled formulas it avoids the complexities of earlier propositional resolution-based methods for modal logic. Third, it pro- vides a method for manipulating so-called assertional information in the description logic setting. And fourth, we believe that it combines ideas from the method of prefixes used in tableaux and resolution in such a way that some of the heuristics and optimizations devised in either field are applicable.

BibTeX

@InCollection{Areces1999g,
  author =       "C. Areces and H. de Nivelle and M. de Rijke",
  booktitle =    "Automated deduction --- CADE-16 (Trento, 1999)",
  title =        "Prefixed resolution: a resolution method for modal and
                 description logics",
  year =         "1999",
  address =      "Berlin, Germany",
  pages =        "187--201",
  abstract =     "We provide a resolution-based proof procedure for
                 modal and description logics that improves on previous
                 proposals in a number of important ways. First, it
                 avoids translations into large undecidable log- ics,
                 and works directly on modal or description logic
                 formulas instead. Second, by using labeled formulas it
                 avoids the complexities of earlier propositional
                 resolution-based methods for modal logic. Third, it
                 pro- vides a method for manipulating so-called
                 assertional information in the description logic
                 setting. And fourth, we believe that it combines ideas
                 from the method of prefixes used in tableaux and
                 resolution in such a way that some of the heuristics
                 and optimizations devised in either field are
                 applicable.",
  publisher =    "Springer",
  ISBN =         "978-3-540-66222-8",
}