ECAI-2002 Conference Paper

[full paper]

Optimised Reasoning for SHIQ

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.