15th European Conference on Artificial Intelligence
|July 21-26 2002 Lyon France|
Ian Horrocks, Ulrike Sattler
We present an optimised version of the tableau algorithm implemented in the FaCT knowledge representation system which decides satisfiability and subsumption in SHIQ, a very expressive description logic providing, e.g., inverse and transitive roles, number restrictions, and general axioms. We prove that the revised algorithm is still sound and complete, and demonstrate that it greatly improves FaCT's performance - in some cases by more than two orders of magnitude.
Keywords: Description Logics, Automated Reasoning, Knowledge Representation
Citation: Ian Horrocks, Ulrike Sattler: Optimised Reasoning for SHIQ . In F. van Harmelen (ed.): ECAI2002, Proceedings of the 15th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2002, pp.277-281.