An ExpTime Tableau Method for Dealing with Nominals and Quantified Number Restrictions in Deciding the Description Logic SHOQ Linh Anh Nguyen1,2 and Joanna Golińska-Pilarek3 1 Institute of Informatics, University of Warsaw Banacha 2, 02-097 Warsaw, Poland nguyen@mimuw.edu.pl 2 Faculty of Information Technology, VNU University of Engineering and Technology 144 Xuan Thuy, Hanoi, Vietnam 3 Institute of Philosophy, University of Warsaw Krakowskie Przedmieście 3, 00-927 Warsaw, Poland j.golinska@uw.edu.pl Abstract. We present the first tableau method with an ExpTime (op- timal) complexity for checking satisfiability of a knowledge base in the description logic SHOQ, which extends ALC with transitive roles, hier- archies of roles, nominals and quantified number restrictions. The com- plexity is measured using binary representation for numbers. Our proce- dure is based on global caching and integer linear feasibility checking. 1 Introduction Description logics (DLs) are formal languages suitable for representing termi- nological knowledge. They are of particular importance in providing a logical formalism for ontologies and the Semantic Web. Automated reasoning in DLs is useful, for example, in engineering and querying ontologies. One of basic reason- ing problems in DLs is to check satisfiability of a knowledge base in a considered DL. Most of other reasoning problems in DLs are reducible to this one. In this paper we study the problem of checking satisfiability of a knowledge base in the DL SHOQ, which extends the basic DL ALC with transitive roles (S), hierarchies of roles (H), nominals (O) and quantified number restrictions (Q). It is known that this problem in SHOQ is ExpTime-complete [16] (even when numbers are coded in binary). Nominals, interpreted as singleton sets, are a useful notion to express identity and uniqueness. However, when interacting with inverse roles (I) and quantified number restrictions in the DL SHOIQ, they cause the complexity of the above mentioned problem to jump up to NExpTime-complete [15] (while that problem in any of the DLs SHOQ, SHIO, SHIQ is ExpTime-complete [16, 7, 15]). In [8] Horrocks and Sattler gave a tableau algorithm for deciding the DL SHOQ(D), which is the extension of SHOQ with concrete datatypes. Later, Pan and Horrocks [13] extended the method of [8] to give a tableau algorithm ExpTime Tableaux for SHOQ 297 for deciding the DL SHOQ(Dn ), which is the extension of SHOQ with n-ary datatype predicates. These algorithms use backtracking to deal with disjunction (t) and “or”-branching (e.g., the “choose”-rule) and use a straightforward way for dealing with with quantified number restrictions. They have a non-optimal complexity (NExpTime) when unary representation is used for numbers, and have a higher complexity (N2ExpTime) when binary representation is used. In [1] Faddoul and Haarslev gave an algebraic tableau reasoning algorithm for SHOQ, which combines the tableau method with linear integer programming. The aim was to increase efficiency of handling quantified number restrictions. However, their algorithm still uses backtracking to deal with disjunction and “or”-branching and has a non-optimal complexity (“double exponential” [1]). In this paper we present the first tableau method with an ExpTime (optimal) complexity for checking satisfiability of a knowledge base in the DL SHOQ. The complexity is measured using binary representation for numbers. Our procedure is based on global caching and integer linear feasibility checking. The idea of global caching comes from Pratt’s work [14] on PDL. It was formally formulated for tableaux in some DLs in [3, 4] and has been applied to several modal and description logics (see [12] for references) to obtain tableau decision procedures with an optimal (ExpTime) complexity. A variant of global caching, called global state caching, was used to obtain cut-free optimal (Exp- Time) tableau decision procedures for several modal logics with converse and DLs with inverse roles [5, 6, 9, 11]. Integer linear programming was exploited for tableaux in [2, 1] to increase ef- ficiency of reasoning with quantified number restrictions. However, the first work that applied integer linear feasibility checking to tableaux was [10, 11]. In [10], Nguyen gave the first ExpTime (optimal) tableau decision procedure for check- ing satisfiability of a knowledge base in the DL SHIQ, where the complexity is measured using binary representation for numbers. His procedure is based on global state caching and integer linear feasibility checking. In the current paper, we apply his method of integer linear feasibility checking to SHOQ. It substan- tially differs from Farsiniamarj’s method of exploiting integer programming for tableaux [2]. Our method of dealing with both nominals and quantified number restrictions is essentially different from the one by Faddoul and Haarslev [1]. Due to the lack of space, we restrict ourselves to introducing the problem of checking satisfiability of a knowledge base in the DL SHOQ and presenting some examples to illustrate our tableau method. For a full description of a tableau decision procedure with an ExpTime complexity we refer the reader to [12]. 2 Notation and Semantics of SHOQ Our language uses a finite set C of concept names, a finite set R of role names, and a finite set I of individual names. A concept name stands for a unary pred- icate, a role name stands for a binary predicate, and an individual name stands for a constant. We use letters like A and B for concept names, r and s for role 298 L.A. Nguyen and J. Golińska-Pilarek names, and a and b for individual names. We also refer to A and B as atomic concepts, to r and s as roles, and to a and b as individuals. An (SHOQ) RBox R is a finite set of role axioms of the form r v s or r ◦ r v r. For example, link v path and path ◦ path v path are such role axioms. By ext(R) we denote the least extension of R such that: – r v r ∈ ext(R) for any role r – if r v r0 ∈ ext(R) and r0 v r00 ∈ ext(R) then r v r00 ∈ ext(R). Let r vR s denote r v s ∈ ext(R), and trans R (r) denote (r◦r v r) ∈ ext(R). If r vR s then r is a subrole of s (w.r.t. R). If trans R (s) then s is a transitive role (w.r.t. R). A role is simple (w.r.t. R) if it is neither transitive nor has any transitive subrole (w.r.t. R). Concepts in SHOQ are formed using the following BNF grammar, where n is a nonnegative integer and s is a simple role: C, D ::= > | ⊥ | A | ¬C | C u D | C t D | ∃r.C | ∀r.C | {a} | ≥ n s.C | ≤ n s.C A concept stands for a set of individuals. The concept > stands for the set of all individuals (in the considered domain). The concept ⊥ stands for the empty set. The constructors ¬, u and t stand for the set operators: comple- ment, intersection and union. For the remaining forms, we give some examples: ∃hasChild .Male, ∀hasChild .Female, ≥ 2 hasChild .Teacher , ≤ 5 hasChild .>. We use letters like C and D to denote arbitrary concepts. . A TBox is a finite set of axioms of the form C v D or C = D. . 6 b. An ABox is a finite set of assertions of the form a : C, r(a, b) or a = . An axiom C v D means C is a subconcept of D, while C = D means C and D are equivalent concepts. An assertion a : C means a is an instance of concept . C, and a =6 b means a and b are distinct individuals. A knowledge base in SHOQ is a tuple hR, T , Ai, where R is an RBox, T is a TBox and A is an ABox. We say that a role s is numeric w.r.t. a knowledge base KB = hR, T , Ai if: – it is simple w.r.t. R and occurs in a concept ≥ n s.C or ≤ n s.C in KB , or – s vR r and r is numeric w.r.t. KB . We will simply call such an s a numeric role when KB is clear from the context. A formula is defined to be either a concept or an ABox assertion. We use letters like ϕ, ψ and ξ to denote formulas. Let null : C stand for C. We use α to denote either an individual or null. Thus, α : C is a formula of the form a : C or null : C (which means C). An interpretation I = h∆I , ·I i consists of a non-empty set ∆I , called the domain of I, and a function ·I , called the interpretation function of I, that maps each concept name A to a subset AI of ∆I , each role name r to a binary relation rI on ∆I , and each individual name a to an element aI ∈ ∆I . The interpretation function is extended to complex concepts as follows, where ]Z ExpTime Tableaux for SHOQ 299 denotes the cardinality of a set Z: >I = ∆I ⊥I = ∅ (¬C)I = ∆I − C I (C u D)I = C I ∩ DI (C t D)I = C I ∪ DI {a}I = {aI } (∃r.C)I = x ∈ ∆I | ∃y hx, yi ∈ rI and y ∈ C I    (∀r.C)I = x ∈ ∆I | ∀y hx, yi ∈ rI implies y ∈ C I    (≥ n s.C)I = x ∈ ∆I | ]{y | hx, yi ∈ sI and y ∈ C I } ≥ n  (≤ n s.C)I = x ∈ ∆I | ]{y | hx, yi ∈ sI and y ∈ C I } ≤ n .  For a set Γ of concepts, define Γ I = {x ∈ ∆I | x ∈ C I for all C ∈ Γ }. The relational composition of binary relations R1 , R2 is denoted by R1 ◦ R2 . An interpretation I is a model of an RBox R if for every axiom r v s (resp. r ◦ r v r) of R, we have that rI ⊆ sI (resp. rI ◦ rI ⊆ rI ). Note that if I is a model of R then it is also a model of ext(R). An interpretation I is a model of a TBox T if for every axiom C v D (resp. . C = D) of T , we have that C I ⊆ DI (resp. C I = DI ). An interpretation I is a model of an ABox A if for every assertion a : C (resp. . 6 b) of A, we have that aI ∈ C I (resp. haI , bI i ∈ rI or aI 6= bI ). r(a, b) or a = An interpretation I is a model of a knowledge base hR, T , Ai if I is a model of R, T and A. A knowledge base hR, T , Ai is satisfiable if it has a model. An interpretation I satisfies a concept C (resp. a set X of concepts) if C I 6= ∅ (resp. X I 6= ∅). It validates C if C I = ∆I . A set X of concepts is satisfiable w.r.t. an RBox R and a TBox T if there exists a model of R and T that satisfies X. For X = A ∪ A0 , where A is an ABox and A0 is a set of assertions of the . form ¬r(a, b) or a = b, we say that X is satisfiable w.r.t. an RBox R and a TBox T if there exists a model I of hR, T , Ai such that: haI , bI i ∈ / rI for all 0 I I . 0 (¬r(a, b)) ∈ A , and a = b for all (a = b) ∈ A . In that case, we also say that I is a model of hR, T , Xi. 3 A Tableau Method for SHOQ We assume that concepts and ABox assertions are represented in negation nor- mal form (NNF), where ¬ occurs only directly before atomic concepts. We use C to denote the NNF of ¬C, and for ϕ = (a : C), we use ϕ to denote a : C. For simplicity, we treat axioms of T as concepts representing global assumptions: . an axiom C v D is treated as C t D, while an axiom C = D is treated as (C t D) u (D t C). That is, we assume that T consists of concepts in NNF. Thus, an interpretation I is a model of T iff I validates every concept C ∈ T . Let EdgeLabels = {testingClosedness, checkingFeasibility}×P(R)×(I∪{null}). For e ∈ EdgeLabels, let e = hπt (e), πr (e), πi (e)i. Thus, πt (e) is the type of e, πr (e) is a set of roles, and πi (e) is either an individual or null. We define a tableaux as a rooted graph. Such a graph is a tuple G = hV, E, νi, where V is a set of nodes, E ⊆ V × V is a set of edges, ν ∈ V is the root, each 300 L.A. Nguyen and J. Golińska-Pilarek node v ∈ V has a number of attributes, and each edge hv, wi may have a number of labels from EdgeLabels. Attributes of a tableau node v are: – Type(v) ∈ {state, non-state}. – SType(v) ∈ {complex, simple} is called the subtype of v. – Status(v) ∈ {unexpanded, p-expanded, f-expanded, closed, open, blocked} ∪ {closed-wrt(U ) | U ⊆ V and Type(u) = state ∧ SType(u) = complex for all u ∈ U }, where p-expanded and f-expanded mean “partially expanded” and “fully expanded”, respectively. Status(v) may be p-expanded only when Type(v) = state. If Status(v) = closed-wrt(U ) then we say that the node v is closed w.r.t. the nodes from U . – Label (v) is a finite set of formulas, called the label of v. – RFmls(v) is a finite set of formulas, called the set of reduced formulas of v. – IndRepl (v) : I → I is a partial mapping specifying replacements of individu- als. It is available only when v is a complex node. If IndRepl (v)(a) = b then, . at the node v, we have a = b and b is the representative of its abstract class. – ILConstraints(v) is a set of integer linear constraints. It is available only when Type(v) = state. The constraints use variables xe indexed by labels e of edges outgoing from v such that πt (e) = checkingFeasibility. Such a variable specifies how many copies of the successor via e will be created for v. If hv, wi ∈ E then we call v a predecessor of w, and w a successor of v. An edge outgoing from a node v has labels iff Type(v) = state. When defined, the set of labels of an edge hv, wi is denoted by ELabels(v, w). If e ∈ ELabels(v, w) then πi (e) = null iff SType(v) = simple. A node v is called a state if Type(v) = state, and non-state otherwise. It is called a complex node if SType(v) = complex, and a simple node otherwise. The label of a complex node consists of ABox assertions, while the label of a simple node consists of concepts. The root ν is a complex non-state. A node may have status blocked only when it is a simple node with the label containing a nominal {a}. The status blocked can be updated only to closed or closed-wrt(. . .). We write closed-wrt(. . .) to mean closed-wrt(U ) for some U . The graph G consists of two layers: the layer of complex nodes and the layer of simple nodes. There are no edges from simple nodes to complex nodes. The edges from complex nodes to simple nodes are exactly the edges outgoing from complex states. That is: if hv, wi is an edge from a complex node v to a simple node w then Type(v) = state; if Type(v) = state and hv, wi ∈ E then SType(w) = simple. Each complex node of G is like an ABox (more formally: its label is an ABox), which can be treated as a graph whose vertices are named individuals. On the other hand, a simple node of G stands for an unnamed individual. If e is a label of an edge from a complex state v to a simple node w then the triple hv, e, wi can be treated as an edge from the named individual πi (e) (an inner node of the graph representing v) to the unnamed individual corresponding to w, and that edge is via the roles from πr (e). We will use also assertions of the form a : ( n s.C) and a : ( n s.C), where s is a numeric role. The difference between a : ( n s.C) and a : (≤ n s.C) is that, for checking a : ( n s.C), we do not have to pay attention to assertions of the ExpTime Tableaux for SHOQ 301 form s(a, b) or r(a, b) with r being a subrole of s. The aim for a : ( n s.C) is similar. We use a : ( n s.C) and a : ( n s.C) only as syntactic representations of some expressions, and do not provide semantics for them. We define FullLabel(v) = Label (v) ∪ RFmls(v) − {formulas of the form a : ( n s.C) or a : ( n s.C)}. We apply global caching: if v1 , v2 ∈ V , Label (v1 ) = Label (v2 ) and (SType(v1 ) = SType(v2 ) = simple or (SType(v1 ) = SType(v2 ) = complex and Type(v1 ) = Type(v2 ))) then v1 = v2 . Due to global caching, an edge outgoing from a state may have a number of labels as the result of merging edges. We say that a node v may affect the status of the root ν if there exists a path consisting of nodes v0 = ν, v1 , . . . , vn−1 , vn = v such that, for every 0 ≤ i < n, Status(vi ) differs from open and closed, and if it is closed-wrt(U ) then U is disjoint from {v0 , . . . , vi }. In that case, if u ∈ {v1 , . . . , vn } then we say that v may affect the status of the root ν via a path through u. From now on, let hR, T , Ai be a knowledge base in NNF of the logic SHOQ, with A 6= ∅. 4 In this section we present a tableau calculus CSHOQ for checking satisfiability of hR, T , Ai. A CSHOQ -tableau for hR, T , Ai is a rooted graph G = hV, E, νi constructed as follows: Initialization: V := {ν}, E := ∅, Type(ν) := non-state, SType(ν) := complex, Status(ν) := unexpanded, RFmls(ν) := ∅, Label (ν) := A ∪ {(a : C) | C ∈ T and a is an individual occurring in A or T }, for each individual a occur- ring in Label (ν) set IndRepl (ν)(a) := a. Rules’ Priorities and Expansion Strategies: The graph is then ex- panded by the following rules, which are specified in detail in [12]: (UPS) rules for updating statuses of nodes, (US) unary static expansion rules, (DN) a rule for dealing with nominals, (NUS) a non-unary static expansion rule, (FS) the forming-state rule, (TP) a transitional partial-expansion rule, (TF) a transitional full-expansion rule. Each of the rules is parametrized by a node v. We say that a rule is applicable to v if it can be applied to v to make changes to the graph. The rule (UPS) has a higher priority than (US), which has a higher priority than the remaining rules in the list. If neither (UPS) nor (US) is applicable to any node, then choose a node v with status unexpanded or p-expanded, choose the first rule applicable to v among the rules in the last five items of the above list, and apply it to v. Any strategy can be used for choosing v, but it is worth to choose v for expansion only when v may affect the status of the root ν of the graph. Note that the priorities of the rules are specified by the order in the above list, but the rules (UPS) and (US) are checked globally (technically, they are triggered immediately when possible), while the remaining rules are checked for a chosen node. 4 If A is empty, we can add a : > to it, where a is a special individual. 302 L.A. Nguyen and J. Golińska-Pilarek Termination: The construction of the graph ends when the root ν receives status closed or open or when no more changes that may affect the status of ν can be made5 . To check satisfiability of hR, T , Ai one can construct a CSHOQ -tableau for it, then return “no” when the root of the tableau has status closed, or “yes” in the other case. It can be proved that (see [12]): – A CSHOQ -tableau for hR, T , Ai can be constructed in ExpTime. – If G = hV, E, νi is an arbitrary CSHOQ -tableau for hR, T , Ai then hR, T , Ai is satisfiable iff Status(ν) 6= closed. Remark 3.1. Our technique for dealing with quantified number restrictions is similar to Nguyen’s technique used for SHIQ [10, 11]. There are some technical differences, which are caused by that we use global caching for SHOQ, while Nguyen’s work [10] uses global state caching for SHIQ (due to inverse roles) and inverse roles can interact with quantified number restrictions. We briefly explain our technique for dealing with nominals. Suppose v is a simple node with Status(v) ∈ / {closed, open} and {a} ∈ Label (v), a complex state u is an ancestor of v, and v may affect the status of the root ν via a path through u. Let u0 be a predecessor of u. The node u0 has only u as a successor and it was expanded by the forming-state rule. There are three cases: – If, for every C ∈ Label (v), the formula obtained from a : C by replacing every individual b by IndRepl (u)(b) belongs to FullLabel(u), then v is “consis- tent” with u. – If there exists C ∈ Label (v) such that the formula obtained from a : C by replacing every individual b by IndRepl (u)(b) belongs to FullLabel(u), then v is “inconsistent” with u. In this case, if Status(v) is of the form closed-wrt(U ) then we update it to closed-wrt(U ∪ {u}), else we update it to closed-wrt({u}). – In the remaining case, the node u is “incomplete” w.r.t. v, which means that the expansion of u0 was not appropriate. Thus, we delete the edge hu0 , ui and re-expand u0 by an appropriate “or”-branching (see [12]). There are also treatments for dealing with assertions of the form a : {b} and for updating statuses of nodes in the presence of closed-wrt(. . .). 2 4 Illustrative Examples Example 4.1. Let us construct a CSHOQ -tableau for hR, T , Ai, where A = {a : A, a : ∃r.∃r.(A t {a}), a : ≥ 3 r.∀r.¬A, a : ∀r.B, a : ≤ 3 r.B, r(a, b), b : ∀r.¬A, b : (∀r.(¬A u ¬{a}) t ¬B)}, R = ∅ and T = ∅. An illustration is presented in Figure 1. 5 That is, ignoring nodes that are unreachable from ν via a path without nodes with status closed or open, no more changes can be made to the graph. ExpTime Tableaux for SHOQ 303 Fig. 1. An illustration of the tableau described in Example 4.1. The marked nodes v4 – v7 and v9 are states. The nodes ν, v1 – v4 are complex nodes, the remaining are simple nodes. In each node, we display the formulas of its label. At the beginning, the graph has only the root ν which is a complex non- state with Label (ν) = A. Since {a : ∀r.B, r(a, b)} ⊂ Label (ν), applying a unary static expansion rule to ν, we connect it to a new complex non-state v1 with Label (v1 ) = Label (ν) ∪ {b : B}. Since b : (∀r.(¬A u ¬{a}) t ¬B) ∈ Label (v1 ), applying the non-unary static expansion rule to v1 , we connect it to new complex non-states v2 and v3 with Label (v2 ) = Label (v1 ) − {b : (∀r.(¬A u ¬{a}) t ¬B)} ∪ {b : ∀r.(¬A u ¬{a})} Label (v3 ) = Label (v1 ) − {b : (∀r.(¬A u ¬{a}) t ¬B)} ∪ {b : ¬B}. 304 L.A. Nguyen and J. Golińska-Pilarek Since both b : B and b : ¬B belong to Label (v3 ), the node v3 receives status closed. Applying the forming-state rule to v2 , we connect it to a new complex state v4 with Label (v4 ) = Label (v2 ) ∪ {a :  1 r.∃r.(A t {a}), a :  2 r.∀r.¬A, a :  2 r.B}. The assertion a :  1 r.∃r.(A t {a}) ∈ Label (v4 ) is due to a : ∃r.∃r.(A t {a}) ∈ Label (v2 ) and the fact that the negation of b : ∃r.(A t {a}) in NNF belongs to Label (v2 ) (notice that r(a, b) ∈ Label (v2 )). The assertion a :  2 r.∀r.¬A ∈ Label (v4 ) is due to a : ≥ 3 r.∀r.¬A ∈ Label (v2 ) and the fact that {r(a, b), b : ∀r.¬A} ⊂ Label (v2 ). Similarly, the assertion a :  2 r.B ∈ Label (v4 ) is due to a : ≤ 3 r.B ∈ Label (v2 ) and the fact {r(a, b), b : B} ⊂ Label (v2 ). As r is a numeric role, applying the transitional partial-expansion rule6 to v4 , we just change the status of v4 to p-expanded. After that, applying the transitional full-expansion rule to v4 , we connect it to new simple non-states v5 , v6 , v7 using edges labeled by e4,5 , e4,6 , e4,7 , respectively, such that e4,i = hcheckingFeasibility, {r}, ai for 5 ≤ i ≤ 7, and Label (v5 ) = {∃r.(A t {a}), B}, Label (v6 ) = {∀r.¬A, B}, Label (v7 ) = {∃r.(A t {a}), ∀r.¬A, B}. The creation of v5 is caused by a :  1 r.∃r.(At{a}) ∈ Label (v4 ), while the creation of v6 is caused by a :  1 r.∀r.¬A. The node v7 results from merging v5 and v6 . Furthermore, ILConstraints(v4 ) consists of xe4,i ≥ 0, for 5 ≤ i ≤ 7, and xe4,5 + xe4,7 ≥ 1 xe4,6 + xe4,7 ≥ 2 xe4,5 + xe4,6 + xe4,7 ≤ 2. Applying the forming-state rule to v5 , the type of this node is changed from non-state to state. Next, applying the transitional partial-expansion rule to v5 , its status is changed to p-expanded. Then, applying the transitional full-expansion rule to v5 , we connect v5 to a new simple non-state v8 with Label (v8 ) = {At{a}} using an edge labeled by e5,8 and set ILConstraints(v5 ) = {xe5,8 ≥ 0, xe5,8 ≥ 1}. Applying the non-unary static expansion rule to v8 , we connect it to new simple non-states v9 and v10 with Label (v9 ) = {A} and Label (v10 ) = {{a}}. The status of v9 is then changed to open, which causes the statuses of v8 and v5 to be updated to open. The node v10 is not expanded as it does not affect the status of the root node ν. Applying the forming-state rule to v6 , the type of this node is changed from non-state to state. Next, applying the transitional partial-expansion rule and then the transitional full-expansion rule to v6 , its status is changed to f-expanded. The status of v6 is then updated to open. Applying the forming-state rule to v7 , the type of this node is changed from non-state to state. Next, applying the transitional partial-expansion rule to v7 , its status is changed to p-expanded. Then, applying the transitional full-expansion rule to v7 , we connect v7 to a new simple non-state v11 with Label (v11 ) = {A t 6 which is used for making transitions via non-numeric roles ExpTime Tableaux for SHOQ 305 {a}, ¬A} using an edge labeled by e7,11 and set ILConstraints(v7 ) = {xe7,11 ≥ 0, xe7,11 ≥ 1}. Applying the non-unary static expansion rule to v11 , we connect it to new simple non-states v12 and v13 with Label (v12 ) = {A, ¬A} and Label (v13 ) = {{a}, ¬A}. The status of v12 is then changed to closed. Since a : A ∈ Label (v4 ), the status of v13 is updated to closed-wrt({v4 }), which causes the status of v11 to be updated also to closed-wrt({v4 }). As the set ILConstraints(v7 ) ∪ {xe7,11 = 0} is infeasible, the status of v7 is updated to closed-wrt({v4 }). Next, as the set ILConstraints(v4 ) ∪ {xe4,7 = 0} is infeasible, the status of v4 is first updated to closed-wrt({v4 }) and then updated to closed. After that, the statuses of v2 , v1 , ν are sequentially updated to closed. Thus, we conclude that the knowledge base hR, T , Ai is unsatisfiable. 2 Example 4.2. Let us modify Example 4.1 by deleting the assertion a : A from the ABox. That is, we are now constructing a CSHOQ -tableau for hR, T , Ai, where A = {a : ∃r.∃r.(A t {a}), a : ≥ 3 r.∀r.¬A, a : ∀r.B, a : ≤ 3 r.B, r(a, b), b : ∀r.¬A, b : (∀r.(¬A u ¬{a}) t ¬B)}, R = ∅ and T = ∅. The first stage of the construction is similar to the one of Example 4.1, up to the step of updating the status of v12 to closed. This stage is illustrated in Figure 2, which is similar to Figure 1 except that the labels of the nodes ν and v1 – v4 do not contain a : A. The continuation is described below and illustrated by Figure 3. Since Label (v13 ) = {{a}, ¬A}, applying the rule for dealing with nominals to v13 , we delete the edge hv2 , v4 i (from E) and re-expand v2 by connecting it to new complex non-states v14 and v15 with Label (v14 ) = Label (v2 ) ∪ {a : ¬A} and Label (v15 ) = Label (v2 ) ∪ {a : A} as shown in Figure 3. The status of v13 is updated to blocked. The node v4 is not deleted, but we do not display it in Figure 3. Applying the forming-state rule to v14 we connect it to a new complex state v16 . The label of v16 is computed using Label (v14 ) in a similar way as in Exam- ple 4.1 when computing Label (v4 ). Applying the transitional partial-expansion rule to v16 we change its status to p-expanded. After that, applying the transitional full-expansion rule to v16 we connect it to the existing nodes v5 , v6 , v7 by using edges labeled by e16,5 , e16,6 , e16,7 , respectively, which are the same tuple hcheckingFeasibility, {r}, ai. The set ILConstraints(v16 ) consists of xe16,i ≥ 0, for 5 ≤ i ≤ 7, and xe16,5 + xe16,7 ≥ 1 xe16,6 + xe16,7 ≥ 2 xe16,5 + xe16,6 + xe16,7 ≤ 2. Applying the forming-state rule to v15 we connect it to a new complex state v17 . The label of v17 is computed using Label (v15 ) in a similar way as in Exam- ple 4.1 when computing Label (v4 ). 306 L.A. Nguyen and J. Golińska-Pilarek Fig. 2. An illustration for Example 4.2 – Part I. The expansion of v17 is similar to the expansion of v16 . The set ILConstraints(v17 ) is like ILConstraints(v16 ), with the subscripts 16 replaced by 17. Analogously to updating the statuses of the nodes v13 , v11 , v7 in Ex- ample 4.1 to closed-wrt({v4 }), the statuses of v13 , v11 , v7 are updated to closed-wrt({v17 }). Next, as ILConstraints(v17 ) ∪ {xe17,7 = 0} is infeasible, the status of v17 is first updated to closed-wrt({v17 }) and then updated to closed. After that, the status of v15 is also updated to closed. As no more changes that may affect the status of ν can be made and Status(ν) 6= closed, we conclude that the knowledge base hR, T , Ai is satisfiable. 2 ExpTime Tableaux for SHOQ 307 Fig. 3. An illustration for Example 4.2 – Part II. 5 Conclusions We have presented the first tableau method with an ExpTime (optimal) com- plexity for checking satisfiability of a knowledge base in the DL SHOQ. The complexity is measured using binary representation for numbers. Our detailed tableau decision procedure for SHOQ is given in [12]. This work differs from Nguyen’s work [10] on SHIQ in that nominals are allowed instead of inverse roles. Without inverse roles, global caching is used in- stead of global state caching to allow more cache hits. To deal with nominals, we use additional statuses closed-wrt(. . .) for nodes of the graph to be constructed. 308 L.A. Nguyen and J. Golińska-Pilarek Acknowledgments. This work was supported by Polish National Science Centre (NCN) under Grants No. 2011/01/B/ST6/02759 (for the first author) and 2011/02/A/HS1/00395 (for the second author). References 1. J. Faddoul and V. Haarslev. Algebraic tableau reasoning for the description logic SHOQ. J. Applied Logic, 8(4):334–355, 2010. 2. N. Farsiniamarj. Combining integer programming and tableau-based reasoning: a hybrid calculus for the description logic SHQ. Master’s thesis, Concordia Univer- sity, 2008. 3. R. Goré and L.A. Nguyen. ExpTime tableaux with global caching for description logics with transitive roles, inverse roles and role hierarchies. In Proceedings of TABLEAUX 2007, volume 4548 of LNAI, pages 133–148. Springer, 2007. 4. R. Goré and L.A. Nguyen. Exptime tableaux for ALC using sound global caching. J. Autom. Reasoning, 50(4):355–381, 2013. 5. R. Goré and F. Widmann. Sound global state caching for ALC with inverse roles. In M. Giese and A. Waaler, editors, Proceedings of TABLEAUX 2009, volume 5607 of LNCS, pages 205–219. Springer, 2009. 6. R. Goré and F. Widmann. Optimal and cut-free tableaux for propositional dynamic logic with converse. In J. Giesl and R. Hähnle, editors, Proceedings of IJCAR 2010, volume 6173 of LNCS, pages 225–239. Springer, 2010. 7. J. Hladik and J. Model. Tableau systems for SHIO and SHIQ. In Proceedings of DL’2004, volume 104 of CEUR Workshop Proceedings, pages 168–177, 2004. 8. I. Horrocks and U. Sattler. Ontology reasoning in the SHOQ(D) description logic. In Proceedings of IJCAI’2001, pages 199–204. Morgan Kaufmann, 2001. 9. L.A. Nguyen. A cut-free ExpTime tableau decision procedure for the description logic SHI. In Proceedings of ICCCI’2011 (1), volume 6922 of LNCS, pages 572–581. Springer, 2011 (see also the long version http://arxiv.org/abs/1106.2305v1). 10. L.A. Nguyen. ExpTime tableaux for the description logic SHIQ based on global state caching and integer linear feasibility checking. arXiv:1205.5838, 2012. 11. L.A. Nguyen. A tableau method with optimal complexity for deciding the de- scription logic SHIQ. In Proceedings of ICCSAMA’2013, volume 479 of Studies in Computational Intelligence, pages 331–342. Springer, 2013. 12. L.A. Nguyen and J. Golińska-Pilarek. A long version of the current paper. http: //www.mimuw.edu.pl/~nguyen/shoq-long.pdf, 2013. 13. J.Z. Pan and I. Horrocks. Reasoning in the SHOQ(Dn ) description logic. In Proc. of DL’2002, volume 53 of CEUR Workshop Proceedings, pages 53–62, 2002. 14. V.R. Pratt. A near-optimal method for reasoning about action. J. Comp. Syst. Sci., 20(2):231–254, 1980. 15. S. Tobies. Complexity results and practical algorithms for logics in knowledge rep- resentation. PhD thesis, RWTH-Aachen, 2001. 16. http://owl.cs.manchester.ac.uk/navigator/.