Tableau Systems for SHIO and SHIQ.

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