EXPtime tableaux for ALC (Q1589576)

The last years have seen two major advances in knowledge representation and reasoning. First, many interesting problems (ranging from semi-structured data to linguistics) were shown to be expressible in logics whose main deductive problems are EXPtime-complete. Second, experiments in automated reasoning have substantially broadened the meaning of ``practical tractability''. Instances of realistic size for Pspace-complete problems are now within reach for implemented systems. Still, there is a gap between the reasoning services needed by the expressive logics mentioned above and those provided by the current systems. Indeed, the algorithms based on tree-automata, which are used to prove EXPtime-completeness, require exponential time and space even in simple cases. On the other hand, current algorithms based on tableau methods can take advantage of such cases, but require double exponential time in the worst case. We propose a tableau calculus for the description logic \(ALC\) for checking the satisfiability of a concept with respect to a TBox with general axioms, and transform it into the first simple tableau-based decision procedure working in single exponential time. To guarantee the ease of implementation, we also discuss the effects that optimizations (propositional backjumping, simplification, semantic branching, etc.) might have on our complexity result, and introduce a few optimizations ourselves.