Tableau Systems for SHIO and SHIQ.

Two prominent families of algorithms for the satisfiability test of DLs are automatabased algorithms (see e.g. [6]), which translate a concept C into an automaton AC accepting all (abstractions of) models for C, and tableau algorithms (TAs) [2], which incrementally create a tree-shaped (pre-) model for C using a set of completion rules. In short, the advantages of automata algorithms are on the theoretical side, because in many cases the proofs are very elegant and provide tight complexity bounds (in particular for ExpTime-complete logics), whereas the advantages of tableau algorithms are on the practical side, since they are well suited for implementation and optimisation. Thus, an approach combining both advantages is highly desirable. In [1], we introduced tableau systems (TSs), a framework for tableau algorithms. From a TS for a DL L, we can derive an automata algorithm deciding satisfiability of L inputs in exponential time, and a tableau algorithm for L, including an appropriate blocking condition which ensures termination. As an application of this framework, we present in this paper tableau systems for two expressive DLs, the new DL SHIO and the wellknown SHIQ [5]. Our main results are the following: firstly, we obtain that SHIO satisfiability is ExpTime-complete and can be decided by a tableau algorithm. Secondly, we will see that although these two logics share most of their constructs, they lead to quite different TSs, which demonstrates how the capabilities of our framework can be used to capture different language properties. Thirdly, the succinctness of the proofs demonstrates how our framework simplifies the design of TAs.