非表示:
キーワード:
-
要旨:
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 logics, 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 provides
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.
