An Abstract Tableau Calculus for the Description Logic SHOI Using Unrestricted Blocking and Rewriting Mohammad Khodadadi, Renate A. Schmidt, and Dmitry Tishkovsky? School of Computer Science, The University of Manchester, UK Abstract This paper presents an abstract tableau calculus for the de- scription logic SHOI. SHOI is the extension of ALC with singleton concepts, role inverse, transitive roles and role inclusion axioms. The presented tableau calculus is inspired by a recently introduced tableau synthesis framework. Termination is achieved by a variation of the un- restricted blocking mechanism that immediately rewrites terms with re- spect to the conjectured equalities. This approach leads to reduced search space for decision procedures based on the calculus. We also discuss re- strictions of the application of the blocking rule by means of additional side conditions and/or additional premises. 1 Introduction Since the late nineteen eighties various tableau algorithms have been developed for description logics [2]. The way they are defined and blocking is performed these tableau algorithms exploit in an essential way that the supported descrip- tion logics have a kind of tree-model property. The basic idea is to perform the derivations such that tree-like models are constructed by systematically creat- ing maximally expanded label sets of concept expressions for individual terms one-by-one in a stratified way. Blocking can then be used to ensure no two in- dividuals (perhaps, in an ancestor relationship) have the same label sets, or are a subset of other label sets. For description logics with role inverse, nominals and number restrictions, this kind of stratified construction is more complex requiring some back-and-forth traversal of a tree model together with forms of dynamic blocking [9,10]. This more complex non-local construction is still aimed at finding tree models and therefore not sufficient for description logics without a kind of tree-model property. In [14,13] we show description logics without the tree-model property, in particular, the description logics ALBO and ALBOid , can be decided using a labelled tableau approach enhanced with the so-called unrestricted blocking mechanism. Labelled tableau approaches are common for modal logics, hybrid logics and various other non-classical logics, cf. e.g., [5,3,4,1]. Labelled tableau approaches are easy to understand, they are easy to define as abstract calculi, ? This research is supported by EPSRC research grant EP/H043748/1. even for undecidable logics, and are not limited to logics with a form of tree model property. There is also more flexibility in the way that derivations can be performed and it is thus easy to devise sound and complete tableau calculi. Building on [14,13] we have devised a framework for systematically developing labelled tableau calculi for various logics, not only description logics [12]. Essen- tially for any logic whose semantic definition can be specified in the specification language of the framework, a sound and complete labelled tableau calculus can be synthesised, if certain general conditions hold. Being based on a sound tableau rule and equality reasoning, the unrestricted blocking mechanism is generally sound and can be incorporated into sound and complete labelled tableau calculi or related approaches. We have shown that if the logic has the finite model property then adding the unrestricted blocking mechanism guarantees also termination [11,12]. Unrestricted blocking provides an intuitively simple method for obtaining termination and behaves very dif- ferent to standard blocking techniques. It does not require specialised blocking tests and complicated dynamic processing steps. All individuals are blockable and once blocked remain blocked. It can be used to find small finite models. The aim of this paper is to formalise reasoning for a well-studied, expres- sive description logic in an abstract labelled tableau calculus incorporating un- restricted blocking. We also we want to explore the possibilities of emulating different kinds of existing blocking techniques. In particular, we present an ab- stract labelled tableau calculus for the description logic SHOI. The tableau calculus is in line with a refined tableau calculus obtained in the tableau syn- thesis framework, but exploiting the tree model property of SHOI, transitive roles are accommodated via a propagation rule rather than a structural rule. Different to most labelled tableau approaches the expansion of ∃ expressions introduces Skolem terms rather than constants. Another novelty is the use of ordered rewriting to realise equality reasoning for singleton concepts (nominals) and blocking. Though there are similarities with substitution and nominal dele- tion approaches (e.g., [10,4,1]), using Skolem terms and ordered rewriting avoids the need to perform again some inference steps on the same branch. Also signifi- cantly fewer inferences are performed than when using standard tableau rules for equality as in, e.g., [3,14,13]. As the unrestricted blocking rule is generally sound, any restriction of the rule obtained by adding side-conditions or premises is also sound. This makes it possible to restrict the application of blocking without losing soundness and completeness. For example, it is possible to approximate standard loop checking techniques such as subset ancestor blocking or anywhere equality blocking and simulate approaches using the δ ∗ -rule. The paper is structured as follows. The syntax and semantics of SHOI are defined in Section 2. In Section 3 we define the tableau calculus for SHOI and in Section 4 we prove that it is sound, complete and terminating. Furthermore, we present examples of restricting the blocking rule by imposing constraints via additional premises and/or side conditions in Section 4. Due to space restrictions we do not discuss the emulation of all known existing blocking techniques but the examples given illustrate the general idea. 2 The Description Logic SHOI SHOI extends the description logic ALC with singleton concepts, role inverse, transitive roles and role inclusion axioms. The language of SHOI is defined over disjoint countable sets of concept names (atomic concepts), individuals, and role names (atomic roles). The symbol A is used to denote an atomic concept, the symbols a and b denote individuals, and the symbol r denotes an atomic role. Concept and role expressions are built from atomic concepts, individuals, and atomic roles using connectives {·} (singleton operator), ¬, t, and ∃ · .· (existential restriction operator), − (role inverse operator). Formally, concept and role expressions are defined respectively by the following grammar rules, where C and D denote concept expressions and R denotes a role expression. def C, D = A | {a} | ¬C | C t D | ∃R.C R = r | R− def The operators >, ⊥, u, and ∀ · .· are defined as usual. In order to simplify the syntax and avoid repetitive occurrences of the role inverse operator we assume def that (r− )− =r. Further, in SHOI, any atomic role is allowed to be declared as transitive and the predicate Trans is used to denote this. Thus, for every atomic role r, Trans(r) is true iff r is transitive. A description logic knowledge base consists of an ABox A, a TBox T and an RBox R. The ABox consists of a finite number of concept assertions of the form a : C and role assertions of the form (a, b) : R. The TBox is used to express a hierarchy between concepts through a finite set of inclusion statements of the form C v D. A normalised TBox is a set of inclusion statements of the form > v C. The RBox is a finite set of inclusion statements of the form R v S and Trans(r), to specify a hierarchy between roles and define transitivity of some roles. We define the closure R+ of the RBox R as the smallest RBox that contains R and satisfies the following properties. – if Q v R ∈ R+ then Q− v R− ∈ R+ ; – if Q v R, R v S ∈ R+ then Q v S ∈ R+ . Given an RBox R, let R∗ denote the RBox R+ ∪ {R v R | R is a role}. The semantics of SHOI is defined by an interpretation I = (∆I , ·I ) given by a pair of a non-empty set ∆I , referred to as the domain of interpretation, and an interpretation function ·I . The function ·I maps individuals to elements of the domain, concept names to subsets of ∆I and role names to binary relations over ∆I . Regarding roles declared as being transitive, ·I must satisfy that rI is a transitive relation whenever Trans(r) is true. The function ·I extends to all concept and role expressions by induction on lengths of expressions as follows: aI = {aI }, (¬C)I = ∆I \ C I , (C t D)I = C I ∪ DI , def def def (∃R.C)I = {x | ∃y ∈ C I (x, y) ∈ RI }, (R− )I = {(x, y) | (y, x) ∈ RI }. def def According to the semantics, the inverse of a role is transitive iff the role is transitive. Following this, we extend the predicate Trans to all role expressions so that Trans(r− ) is true iff Trans(r) is true. Let E denote any concept expression, any concept inclusion, any role inclu- sion, any concept assertion or any role assertion. We indicate by I |= E that E is valid in the model I. We define: def def I |= C ⇐⇒ C I = ∆I I |= a : C ⇐⇒ aI ∈ C I def def I |= R v S ⇐⇒ RI ⊆ S I I |= (a, b) : R ⇐⇒ (aI , bI ) ∈ RI def I |= C v D ⇐⇒ C I ⊆ DI Because SHOI supports singleton concepts, every ABox statement a : C can be encoded by the TBox statement {a} v C. Also, every role assertion (a, b) : R can be encoded as the TBox statement {a} v ∃R.{b}. Thus, without loss of generality, we assume that a knowledge base is a pair (T , R) which consists of a normalised TBox T and an RBox R. It worth noting that the TBox can be internalised as well [15] but for performance reasons we present a tableau calculus that handles TBox statements directly. A concept C is satisfiable in a model I iff C I 6= ∅. A concept is satisfiable in I with respect to a knowledge base if it is satisfiable in I whenever every statement of the knowledge base is valid in I. That is, C is satisfiable with respect to (T , R) in I iff C I 6= ∅ provided that I |= E for every E ∈ T ∪ R. 3 An Abstract Tableau Calculus for SHOI In this section we present a labelled semantic ground tableau calculus for SHOI. The language of the tableau calculus is an extension of the language of SHOI with equality formulae and individual terms used as labels. We add a function symbol f which takes a triple (s, R, C) consisting of an individual term s, a role expression R and a concept expression C as its arguments and define the set of (individual) terms s inductively by the following grammar rule, where a denotes any individual, C any concept and R any role. def s = a | f (s, R, C) Terms which are not ABox individuals can be viewed as being Skolem terms. Formulae in the tableau language are defined by the following grammar rule, where s and t are individual terms, C is a concept and R is a role. def E = s : C | (s, t) : R | s ≈ t We extend the interpretation of SHOI expressions to the formulae of the tableau language. For every SHOI interpretation I, let the interpretation f I in I of the function f be an arbitrary function mapping triples (x, ρ, χ) with x ∈ ∆I , ρ ⊆ (∆I )2 , χ ⊆ ∆I to elements of ∆I . We let (f (a, R, C))I = f I (aI , RI , C I ), I |= (s : C)I ⇐⇒ sI ∈ C I , def def I |= s ≈ t ⇐⇒ sI = tI , I |= (s, t) : R ⇐⇒ (sI , tI ) ∈ RI . def def The interpretations of the formulae s ≈ t, s : {t} and t : {s} coincide. In accordance with their interpretation we refer to these formulae as equalities. We also refer to the formulae of the form s : ¬{t} as inequalities. Let Tab denote a tableau calculus comprising of a set of inference rules. A derivation or tableau for Tab is a finitely branching, ordered tree whose nodes are annotated by sets of tableau formulae. Assuming that C is the input concept expression to be tested for satisfiability with respect a knowledge base (T , R) the root node of the tableau is the set {a : C}, where a denotes a fresh individual. Successor nodes are constructed in accordance with a set of inference rules in the calculus. The inference rules have the general form X0 (side-condition), X1 | . . . | Xn where X0 is the set of premises and the Xi are the sets of conclusions. If n = 0, the rule is called closure rule and written X0 /⊥. If σ is a substitution that acts on tableau formulae and X = {E1 , . . . , Ek } is a set of tableau formulae then Xσ denotes the set {E1 σ, . . . , Ek σ}. A rule is applicable to a tableau if there is a leaf node annotated with a set N and there is a substitution σ such that X0 σ ⊆ N , where X0 is the set of premises of the rule, and the side-condition of the rule is true for N . σ is called the matching substitution of the rule application. We assume in a rule individual symbols, concept symbols and role symbols represent variables that are matched with individual terms, concept expressions and role expressions respectively. We also say the rule is applicable to the formulae X0 σ in (the leaf node of) the branch. If a rule of the calculus is applicable to a leaf node of the tableau with a matching substitution σ, then the tableau is extended by attaching to the leaf node n child nodes annotated with N ∪ Xi σ for i = 1, . . . n, respectively. In order to avoid redundancies we stipulate that a rule application to a leaf node annotated with N is redundant if there is a conclusion set Xi for some i = 1, . . . n of the rule such that Xi σ ⊆ N , where σ is the matching substitution. This ensures rules are not applied more than once to the same sets of formulae. A branch in the tableau is a maximal path from the root of the tableau to a leaf node. If a closure rule has been applied in a branch then the branch is said to be closed. If a branch is not closed, it is called open. A tableau is closed if all its branches are closed. A branch is fully expanded if no more rules are applicable to its leaf node modulo redundancy. We call a tableau fully expanded iff all its branches are fully expanded. We denote by Tab(T , R, C) a fully ex- panded tableau constructed in the calculus Tab for the input concept C and the knowledge base (T , R). We need equality reasoning for individual terms to achieve termination for the calculus. Equality reasoning can be provided in various ways. One is to supply special tableau rules for reasoning modulo equalities within the branch in a similar way as is done in [3,14,13]. Another is to use ordered term rewriting. Ordered rewriting is more efficient for handling equal individuals because it allows to reduce the number of tableau formulae in the current branch. Since s : ¬C, s : C s : ¬¬C (⊥): (¬¬): ⊥ s:C s:C tD s : ¬(C t D) (t): (¬t): s:C|s:D s : ¬C, s : ¬D s : ∃R.C − (s, t) : R− (∃): ( ): f (s, R, C) : C, (s, f (s, R, C)) : R (t, s) : R s : ¬∃S.C, (s, t) : R s:C (¬∃): (R v S ∈ R∗ ) (id): t : ¬C s : {s} s : ¬∃S − .C, (t, s) : R s : ¬{t} (¬∃− ): (R v S ∈ R∗ ) (id2 ): t : ¬C t : {t} s : ¬∃S.C, (s, t) : R (s, t) : R (+ ): (R v S ∈ R∗ , Trans(R) ∈ R) (cng): t : ¬∃R.C s : {s}, t : {t} s : ¬∃S − .C, (t, s) : R s : {s} (−+ ): (R v S ∈ R∗ , Trans(R) ∈ R) (TBox): (C ∈ T ) t : ¬∃R− .C s:C (s, t) : R s : {t} (RBox): (R v S ∈ R+ ) (≈): (s 6= t) (s, t) : S s≈t Figure 1. The tableau calculus TabSHOI all individual terms in any tableau derivation are ground we are dealing with a special case of rewriting, namely, ground rewriting. In this paper, a rewrite system R is a binary relation on the set of all indi- vidual terms and consists of rewrite rules which are pairs of individual terms. In order to handle equalities, we orient each equality formula appearing in the current branch of a tableau derivation according to a special ordering  which is a strict partial order on individual terms. We denote by s → t a rewrite rule (s, t) in which s  t. Thus, if an equality formula s ≈ t appears in a node of a branch then either s → t or t → s is added as a rewrite rule to the rewrite system of the branch. A term which cannot be rewritten (with respect to a rewrite system) is said to be in normal form. A normal form of a term s is denoted by nf(s). A rewrite system is terminating if there is a normal form for each term. Our tableau calculus TabSHOI for the description logic SHOI is given in Figure 1. The (⊥) rule is the closure rule. The (¬¬) rule removes occurrences of double negation on concepts. The (t) and (¬t) rules are standard rules for handling concept disjunctions. Given a tableau formula s : ∃R.C, the (∃) rule introduces an individual term f (s, R, C) as an R-successor of s (instead of intro- ducing a fresh individual as might be done in other presentations). The (¬∃) rule is equivalent to the standard rule for universally restricted concept expressions. The (¬∃− ) rule allows the backward propagation of concept expressions along inverted links. The (− ) rule inverts a given link. The (+ ) rule propagates negated existential concept restriction along a tran- sitive link while the (−+ ) rule does the same for inverse occurrences of transitive roles. Equalities of the form s : {s} are tautologies, used in our calculus as do- main predicates for keeping track of the terms that have been introduced to a branch. This is achieved with the three rules (id), (id2 ) and (cng). The (TBox) rule concatenates every concept of the normalised TBox with every label occur- ring on the branch. The (RBox) propagates a link of a role into its superrole according to the closure R+ of the given RBox R. The (≈) rule is a special rule adding, what we call, a rewrite trigger s ≈ t to the branch. Let  be any reduction ordering on the set of individuals in the branch. The addition of any tableau formula s ≈ t to a set N of formulae which annotates a leaf tableau node immediately triggers the following rewrite process. Suppose that s  t (the case t  s is symmetrical). Then, s → t is added to a rewrite system R associated with the current tableau branch. The tableau is extended by attaching one child node to the current leaf node. The child node is annotated by the set N 0 obtained by rewriting all the tableau formulae in N with respect to the rewrite system R. In particular, this means that, in N 0 every ∗ term s is replaced by a term u such that s → u with respect to R. 4 Soundness, Completeness and Termination It is not difficult to see that each rule of TabSHOI is sound, i.e., preserves satisfiability of concept assertions. Consequently: Theorem 1 (Soundness). The tableau calculus TabSHOI is sound for the de- scription logic SHOI. That is, if a concept C is satisfiable with respect to the knowledge base (T , R) then any fully expanded TabSHOI -tableau for (T , R, C) has an open branch. A tableau calculus Tab is complete iff for every knowledge base (T , R) and every concept C if C is unsatisfiable with respect to (T , R) then there is a closed tableau Tab(T , R, C). In order to prove completeness of TabSHOI , we prove its constructive completeness which implies completeness. A tableau calculus Tab is constructively complete if for every open branch in any fully expanded tableau Tab(T , R, C) there is a model which validates the knowledge base (T , R) and satisfies C. Theorem 2 (Completeness). TabSHOI is a (constructively) complete tableau calculus for the description logic SHOI. Next, we establish termination. A tableau calculus Tab is (weakly) termi- nating if any tableau Tab(T , R, C) has a finite open branch provided that C is satisfiable concept with respect to the knowledge base (T , R). Although TabSHOI is a sound and complete tableau calculus for the descrip- tion logic SHOI, it is not terminating. In order to achieve termination, a form of blocking or loop-checking is necessary. One possibility is to add the unrestricted blocking mechanism described in [14]. As is shown in [12], this will ensure ter- mination of an arbitrary tableau calculus under certain conditions, one of which being condition (c2) discussed below. In this paper, we take a slightly different route and introduce a modified version of the unrestricted blocking mechanism. It is given by the (ub-rw) rule and ordered rewriting. s : {s}, t : {t} (ub-rw): (s 6= t) s ≈ t | s : ¬{t} Here, s ≈ t is a rewrite trigger as introduced in Section 3. Premises of this rule are instantiated with any two distinct terms s and t used as labels in a set of tableau formulae N annotating the current leaf node. As a result of a rule application two successor nodes are created. If s  t (respectively t  s) then in the left node a rewrite rule s → t (respectively t → s) is added to the rewrite system R. The left node is annotated with a copy of N , which is rewritten with respect to the newly obtained rewrite system R. The right node is annotated with a copy of N extended with the additional formula s : ¬{t}. This formula indicates the case that s and t are not equal. The calculus consisting of all the rules of TabSHOI and the rule (ub-rw) is denoted by TabSHOI (ub-rw). Clearly, the (ub-rw) rule is sound. Therefore: Theorem 3. The calculus TabSHOI (ub-rw) is a sound and (constructively) complete for the description logic SHOI. In order to ensure termination for a procedure based on TabSHOI (ub-rw) the rule application strategy must satisfy the following condition. (c2) In every open branch there is some node from which point onward before any application of the (∃) rule all possible applications of the (ub-rw) rule have been performed. (The unrestricted blocking mechanism in [14] also needs to satisfy a second condition, which is already satisfied in our modified setting.) Provided that condition (c2) holds, a sufficient and necessary condition for termination of the tableau procedures based on TabSHOI (ub-rw) is that SHOI has the finite model property with respect to its standard semantics. This can be shown in a similar way as in [13]. A description logic has the finite model property if for an arbitrary concept C and arbitrary knowledge base it holds that if C is satisfiable with respect to the knowledge base in a model for the logic then C is satisfiable with respect to the knowledge base in a finite model of the logic. The finite model property for SHOI can be shown by a filtration argument. Theorem 4 (Finite model property of SHOI). The description logic SHOI has the finite model property. Therefore, using the results of [13] we obtain the following theorem. Theorem 5 (Termination). Any implementation, fair in the sense of [13], of the tableau calculus TabSHOI (ub-rw) and satisfies condition (c2) is a decision procedure for SHOI and its sublogics. 5 Sound Restricted Blocking The (ub-rw) rule creates potentially many branching points in a derivation, especially if the number individuals and ∃-expressions in the knowledge base is high. A way to reduce the number of applications of the (ub-rw) rule and thus reduce the search space is to apply the blocking rule less often. This can be achieved by adding side-conditions and/or premises to the rule. Ideal would be side-conditions and additional premises that maximise the chance of constructing a finite model without the need for backtracking. In the remaining section, we give some examples of restricted versions of the (ub-rw) rule. They all preserve soundness and completeness. We have: Theorem 6 (Soundness and completeness). The (ub-rw) rule constrained by additional premises or side-conditions is sound. Thus, TabSHOI extended with such a modified rule is sound and complete for SHOI. Most existing description logic tableau algorithms aim to construct models given by relational tree structures where the nodes are individuals (or individual terms, if Skolem terms would have been used) and are annotated with label sets def of concept expressions. A label set of a term s is the set L(s)={C | s : C ∈ N }. These label sets are then used in the tests of standard blocking mechanism such as subset ancestor blocking and dynamic anywhere equality blocking. An emulation of subset ancestor blocking can be realised through the selective application of the (ub-rw) rule, realised by adding a side-condition: s : {s}, t : {t} (ub⊆ -rw): (s 6= t, s is an ancestor of t and L(t) ⊆ L(s)) s ≈ t | s : ¬{t} In this rule the application of the (ub-rw) rule is restricted to a term s and its successor term t, where the label set of s is a superset of the label set of t. In our setting, as the calculus creates Skolem terms in the (∃) rule, a term s is an ancestor of a term t, if s is a subterm of t. Standard ancestor subset blocking is used in tableau algorithms for descrip- tion logics ALC, S and SH [7]. In ancestor subset blocking, a term t is blocked by its ancestor s if L(t) ⊆ L(s). No rule is applicable to the blocked individ- uals. As standard ancestor blocking is not a branching rule it is important to perform the expansions in a stratified way and perform the subset test at an appropriate moment in order to preserve soundness. But even if the expansions are performed in the required way standard ancestor blocking is not generally sound unlike blocking based on the (ub⊆ -rw) rule. Application of the (ub-rw) rule can be limited by ignoring the pairs of terms where the application of the rule is not critical for termination. E.g., it is possi- ble to ignore pairs where both terms appear before some fixed node of a tableau derivation. We believe, as there are a finite number of individuals before a fixed tableau node, excluding them does not endanger termination. In particular, the pairs where both terms are ABox individuals can be ignored as in [8]. If the unique name assumption is assumed for the given ABox individuals, identify- ing these individuals by blocking would be incorrect. Using the following rule instead of using the (ub-rw) rule can have a significant impact on the perfor- mance, especially when reasoning over knowledge bases with a large number of individuals. s : {s}, t : {t} (ubNo ABox -rw): (s 6= t, not both s and t are ABox individuals) s ≈ t | s : ¬{t} We can define a variation of the (ub-rw) rule restricted to the terms that are known to be the ones that may cause infinite derivations. For TabSHOI , infinite derivations can be caused only by infinite applications of the (∃) rule. This means we may focus blocking on the terms to which the (∃) rule may eventually be applicable, i.e., the terms which have an ∃-expression in their label sets. We may formulate the (ub-rw) rule as follows to reflect this restriction: s : ∃R.C, t : ∃S.D (ub∃ -rw): (s 6= t) s ≈ t | s : ¬{t} Here, ∃R.C, ∃S.D are two ∃-expression that can be matched with any ∃-expres- sion. This rule is applicable to any pair of terms s and t which both have a ∃-expression in their label sets. The three variations of the (ub-rw) rule just presented are all sound, thus preserving soundness (and completeness) of the calculus is not an issue. An issue is to show under which conditions and for which logics termination can be ensured. Because of the side-conditions or additional premises these variations of the (ub-rw) rule are no longer applied to every possible pair of terms. Thus, condition (c2) does not hold. We believe however it can be proved that search strategies can be adopted where blocking applies to sufficiently many pairs so that the procedure terminates. Next we illustrate how the (δ ∗ ) rule [6] can be simulated using a restriction of the (ub-rw) rule. The (δ ∗ ) rule systematically reuses terms in order to find finite models. For description logics the (δ ∗ ) rule is defined as follows: ∗ s : ∃R.C (δ ): (s, t1 ) : R, t1 : C | · · · | (s, tn ) : R, tn : C | (s, f (s, R, C)) : R, f (s, R, C) : C Here, t1 , . . . , tn are all existing terms, covering all given ABox individuals and all introduced Skolem terms on the current branch. The (δ ∗ ) rule is actually a modified version of the (∃) rule. Instead of creating a new term to satisfy an ∃-expression, this rule tries to satisfy the ∃-expression by reusing existing terms. If all the attempts to satisfy the ∃-expression with existing terms end in contradictions, then a new term f (s, R, C) is introduced. In our abstract calculus we can simulate the (δ ∗ ) rule with the (∃) rule and modifying the (ub-rw) rule to: s : {s}, t : {t} (ubδ∗ -rw): (s 6= t, t is a Skolem term) s ≈ t | s : ¬{t} We should use a rule application strategy where after each application of the (∃) rule, the (ubδ∗ -rw) rule is applied to the newly added Skolem term and every existing term. In contrast to the previous blocking variations, the (ubδ∗ -rw) rule satisfies condition (c2), since all possible term comparisons are performed before any application of the (∃) rule. Hence termination is ensured. Theorem 7 (Termination). Any implementation, fair in the sense of [13], of the tableau calculus TabSHOI extended with the (ubδ∗ -rw) rule and using the described strategy is a decision procedure for SHOI and its sublogics. 6 Concluding Remarks The contribution of this paper is an abstract labelled tableau calculus for the description logic SHOI using ordered rewriting and generic forms of blocking defined as variations of the unrestricted blocking mechanism. The tableau cal- culus is designed to be as general as possible in order to gain greater insight into minimal requirements for soundness, completeness and termination and con- duct the proofs without any considerations for search strategies, heuristics and other implementation issues. The discussion in [13] of how to obtain determin- istic tableau procedures for implementation based on the notion of fairness as defined in that paper carries over to the calculi presented here. We hope this ongoing work will lead to even greater insight of the theory and techniques of different tableau approaches for description logics and their implementation. References 1. Alenda, R., Olivetti, N., Schwind, C., Tishkovsky, D.: Tableau calculi for CSL over min-spaces. In: Proc. CSL’10. LNCS, vol. 6247, pp. 52–66. Springer (2010) 2. Baader, F., Sattler, U.: An overview of tableau algorithms for description logics. Studia Logica 69(1), 5–40 (2001) 3. Bolander, T., Blackburn, P.: Termination for hybrid tableaus. J. Logic Comput. 17(3), 517–554 (2007) 4. Cialdea Mayer, M., Cerrito, S.: Nominal substitution at work with the global and converse modalities. In: Proc. AiML-8. pp. 57–74. College Publ. (2010) 5. Fitting, M.: Proof methods for modal and intuitionistic logics. Kluwer (1983) 6. Hintikka, J.: Model minimization: An alternative to circumscription. J. Automat. Reason. 4(1), 1–13 (1988) 7. Horrocks, I.: Using an expressive description logic: FaCT or fiction? In: Proc. KR- 98. pp. 636–647. Morgan Kaufmann (1998) 8. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Proc. KR 2006. pp. 57–67. AAAI Press (2006) 9. Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and role hierarchies. J. Logic Comput. 9(3), 385–410 (1999) 10. Horrocks, I., Sattler, U.: A tableau decision procedure for SHOIQ. J. Automat. Reason. 39(3), 249–276 (2007) 11. Schmidt, R.A., Tishkovsky, D.: A general tableau method for deciding description logics, modal logics and related first-order fragments. In: Proc. IJCAR’08. LNCS, vol. 5195, pp. 194–209. Springer (2008) 12. Schmidt, R.A., Tishkovsky, D.: Automated synthesis of tableau calculi. Logical Methods in Comput. Sci. 7(2), 1–32 (2011) 13. Schmidt, R.A., Tishkovsky, D.: Using tableau to decide description logics with full role negation and identity (2011), manuscript, http://www.mettel-prover.org/ papers/ALBOid.pdf 14. Schmidt, R.A., Tishkovsky, D.: Using tableau to decide expressive description logics with role negation. In: Proc. ISWC+ASWC’07. pp. 438–451. Springer (2007) 15. Tobies, S.: The complexity of reasoning with cardinality restrictions and nominals in expressive description logics. J. Artificial Intelligence Res. 12, 199–217 (2000)