View article

The description logic extends the basic description logic with transitive roles, role hierarchies and inverse roles. The known tableau-based decision procedure [9] for exhibit (at least) NEXPTIME behaviour even though is known to be EXPTIME-complete. The automata-based algorithms for often yield optimal worst-case complexity results, but do not behave well in practice since good optimisations for them have yet to be found. We extend our method for global caching in to by adding analytic cut rules, thereby giving the first EXPTIME tableau-based decision procedure for , and showing one way to incorporate global caching and inverse roles.