Optimised reasoning for SHIQ

We present an optimised version of the tableau algorithm implemented in the FaCT knowledge representation system which decides satisfiability and subsumption in SHLQ, 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.