Prefixed resolution: A resolution method for modal and description logics

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.