Comparing Subsumption Optimizations

Effective systems for expressive description logics require a heavily-optimised subsumption checker incorporating a range of optimisation techniques. Because of the correspondence between description logics and propositional modal logic most of these techniques carry over into propositional modal logic satisfiability checking. Some of the techniques are extremely effective on various test suites for propositional modal satisfiability and others are less effective. Further, the effectiveness of a technique depends on the test performed. Description logic systems spend much of their time computing subsumption relationships between descriptions. If the system is based on an expressive description logic then the amount of time spent computing subsumption can be intolerable, even for small knowledge bases, unless steps are taken to heavily optimise this task. The total time spent in subsumption checking comes from the number of subsumption checks required to process a knowledge base as wel...

• Type: Conference
• Year: 1998
• Where: DLOG
• Authors: Ian Horrocks, Peter F. Patel-Schneider
• Keywords: Automated Reasoning, Description Logic, DLOG 1998, Expressive Description Logic, Subsumption Check