Optimising Propositional Modal Satisfiability for Description Logic Subsumption

Effective optimisation techniques can make a dramatic difference in the performance of knowledge representation systems based on expressive description logics. Because of the correspondence between description logics and propositional modal logic many of these techniques carry over into propositional modal logic satisfiability checking. Currently-implemented representation systems that employ these techniques, such as FaCT and DLP, make effective satisfiable checkers for various propositional modal logics.

• Type: Conference
• Year: 1998
• Where: AISC
• Authors: Ian Horrocks, Peter F. Patel-Schneider
• Keywords: AISC 1998, Artificial Intelligence, Description Logics, Modal Logic Satisfiability, Propositional Modal Logics