We present the rst tableau method with an ExpTime (optimal) complexity for checking satis ability of a knowledge base in the description logic SHOQ, which extends ALC with transitive roles, hierarchies of roles, nominals and quanti ed number restrictions. The complexity is measured using binary representation for numbers. Our procedure is based on global caching and integer linear feasibility checking.
Description logics (DLs) are formal languages suitable for representing terminological 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 reasoning problems in DLs is to check satis ability 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 satis ability 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 quanti ed number restrictions (Q).
It is known that this problem in SHOQ is ExpTime-complete [
Nominals, interpreted as singleton sets, are a useful notion to express identity
and uniqueness. However, when interacting with inverse roles (I) and quanti ed
number restrictions in the DL SHOIQ, they cause the complexity of the above
mentioned problem to jump up to NExpTime-complete [
In [
In this paper we present the rst tableau method with an ExpTime (optimal) complexity for checking satis ability 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 [
Integer linear programming was exploited for tableaux in [
Due to the lack of space, we restrict ourselves to introducing the problem of
checking satis ability 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 [
Our language uses a nite set C of concept names, a nite set R of role names, and a nite set I of individual names. A concept name stands for a unary predicate, 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 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 nite 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 2 ext (R) for any role r { if r v r0 2 ext (R) and r0 v r00 2 ext (R) then r v r00 2 ext (R).
Let r vR s denote r v s 2 ext (R), and transR(r) denote (r r v r) 2 ext (R). If r vR s then r is a subrole of s (w.r.t. R). If transR(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 ::= > j ? j A j :C j C u D j C t D j 9r:C j 8r:C j fag j n s:C j 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: complement, intersection and union. For the remaining forms, we give some examples: 9hasChild :Male, 8hasChild :Female, 2 hasChild :Teacher , 5 hasChild :>.
We use letters like C and D to denote arbitrary concepts.
A TBox is a nite set of axioms of the form C v D or C =: D. : An ABox is a nite set of assertions of the form a : C, r(a; b) or a 6= b.
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 { s vR r and r is numeric w.r.t. KB . n s:C or n s:C in KB , or We will simply call such an s a numeric role when KB is clear from the context.
A formula is de ned 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 2 I . The interpretation function is extended to complex concepts as follows, where ]Z denotes the cardinality of a set Z: For a set of concepts, de ne I = fx 2 I j x 2 CI for all C 2 g. 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 CI DI (resp. CI = DI ).
An interpretation I is a model of an ABox A if for every assertion a : C (resp.
: r(a; b) or a 6= b) of A, we have that aI 2 CI (resp. haI ; bI i 2 rI or aI 6= bI ).
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 satis able if it has a model.
An interpretation I satis es a concept C (resp. a set X of concepts) if CI 6= ; (resp. XI 6= ;). It validates C if CI = I . A set X of concepts is satis able w.r.t. an RBox R and a TBox T if there exists a model of R and T that satis es fXor.mFo:r rX(a;=b) Aor[aA=0:, wb,hweree sAayisthaant AXBoisx saantdis Aable w.r.t. an RBox R and a 0 is a set of assertions of the TBox T if there exists a model I of hR; T ; Ai such that: haI ; bI i 2= rI for all : (:r(a; b)) 2 A0, and aI = bI for all (a = b) 2 A0. In that case, we also say that I is a model of hR; T ; Xi. 3
We assume that concepts and ABox assertions are represented in negation normal 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 glo:bal 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 i I validates every concept C 2 T .
Let EdgeLabels = ftestingClosedness; checkingFeasibilityg P(R) (I[fnullg). For e 2 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 de ne 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, 2 V is the root, each node v 2 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) 2 fstate; non-stateg. { SType(v) 2 fcomplex; simpleg is called the subtype of v. { Status(v) 2 funexpanded, p-expanded, f-expanded, closed, open, blockedg [ fclosed-wrt(U ) j U V and Type(u) = state ^ SType(u) = complex for all u 2 U g, 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 nite set of formulas, called the label of v. { RFmls(v) is a nite set of formulas, called the set of reduced formulas of v. { IndRepl (v) : I ! I is a partial mapping specifying replacements of individuals. 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 speci es how many copies of the successor via e will be created for v.
If hv; wi 2 E then we call v a predecessor of w, and w a successor of v. An edge outgoing from a node v has labels i Type(v) = state. When de ned, the set of labels of an edge hv; wi is denoted by ELabels(v; w). If e 2 ELabels(v; w) then i(e) = null i 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 a . The status blocked can be updated only to closed or containing a nominal f g 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 2 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 di erence 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 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 de ne FullLabel(v) = Label (v) [ RFmls(v)
fformulas of the form a : ( n s:C) or a : ( n s:C)g:
We apply global caching: if v1; v2 2 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 a ect 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) di ers from open and closed, and if it is closed-wrt(U ) then U is disjoint from fv0; : : : ; vig. In that case, if u 2 fv1; : : : ; vng then we say that v may a ect 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 satis ability of hR; T ; Ai. A CSHOQ-tableau for hR; T ; Ai is a rooted graph G = hV; E; i constructed as follows:
Initialization: V := f g, E := ;, Type( ) := non-state, SType( ) := complex, Status( ) := unexpanded, RFmls( ) := ;, Label ( ) := A [ f(a : C) j C 2 T and a is an individual occurring in A or T g, for each individual a occurring in Label ( ) set IndRepl ( )(a) := a.
Rules' Priorities and Expansion Strategies: The graph is then
expanded by the following rules, which are speci ed in detail in [
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 rst rule applicable to v among the rules in the last ve 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 a ect the status of the root of the graph. Note that the priorities of the rules are speci ed 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.
Termination: The construction of the graph ends when the root receives status closed or open or when no more changes that may a ect the status of can be made5.
To check satis ability 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 [
Remark 3.1. Our technique for dealing with quanti ed number restrictions is
similar to Nguyen's technique used for SHIQ [
We brie y explain our technique for dealing with nominals. Suppose v is
a simple node with Status(v) 2= fclosed; openg and fag 2 Label (v), a complex
state u is an ancestor of v, and v may a ect 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 2 Label (v), the formula obtained from a : C by replacing every
individual b by IndRepl (u)(b) belongs to FullLabel(u), then v is
\consistent" with u.
{ If there exists C 2 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 [ fug), else we update it to
closed-wrt(fug).
{ 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 [
There are also treatments for dealing with assertions of the form a : fbg and for updating statuses of nodes in the presence of closed-wrt(: : :). 2 4
Example 4.1. Let us construct a CSHOQ-tableau for hR; T ; Ai, where A = fa : A; a : 9r:9r:(A t fag); a : 3 r:8r::A; a : 8r:B; a : 3 r:B; r(a; b); b : 8r::A; b : (8r:(:A u :fag) t :B)g; 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.
At the beginning, the graph has only the root which is a complex nonstate with Label ( ) = A. Since fa : 8r:B; r(a; b)g Label ( ), applying a unary static expansion rule to , we connect it to a new complex non-state v1 with Label (v1) = Label ( ) [ fb : Bg.
Since b : (8r:(:A u :fag) t :B) 2 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) Label (v3) = Label (v1) fb : (8r:(:A u :fag) t :B)g [ fb : 8r:(:A u :fag)g fb : (8r:(:A u :fag) t :B)g [ fb : :Bg:
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) [ fa : 1 r:9r:(A t fag); a : 2 r:8r::A; a : 2 r:Bg: The assertion a : 1 r:9r:(A t fag) 2 Label (v4) is due to a : 9r:9r:(A t fag) 2 Label (v2) and the fact that the negation of b : 9r:(A t f g a ) in NNF belongs to Label (v2) (notice that r(a; b) 2 Label (v2)). The assertion a : 2 r:8r::A 2 Label (v4) is due to a : 3 r:8r::A 2 Label (v2) and the fact that fr(a; b), b : 8r::Ag Label (v2). Similarly, the assertion a : 2 r:B 2 Label (v4) is due to a : 3 r:B 2 Label (v2) and the fact fr(a; b); b : Bg 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; frg; ai for 5 i 7, and Label (v5) = f9r:(A t fag); Bg, Label (v6) = f8r::A; Bg, Label (v7) = f9r:(A t fag); 8r::A; Bg. The creation of v5 is caused by a : 1 r:9r:(Atfag) 2 Label (v4), while the creation of v6 is caused by a : 1 r:8r::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 xe4;6 + xe4;7 xe4;5 + xe4;6 + xe4;7
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) = fAtfagg using an edge labeled by e5;8 and set ILConstraints (v5) = fxe5;8 0; xe5;8 1g.
Applying the non-unary static expansion rule to v8, we connect it to new simple non-states v9 and v10 with Label (v9) = fAg and Label (v10) = ffagg. 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 a ect 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) = fA t 6 which is used for making transitions via non-numeric roles fag; :Ag using an edge labeled by e7;11 and set ILConstraints (v7) = fxe7;11 0, xe7;11 1g.
Applying the non-unary static expansion rule to v11, we connect it to new simple non-states v12 and v13 with Label (v12) = fA; :Ag and Label (v13) = ffag; :Ag. The status of v12 is then changed to closed. Since a : A 2 Label (v4), the status of v13 is updated to closed-wrt(fv4g), which causes the status of v11 to be updated also to closed-wrt(fv4g). As the set ILConstraints (v7) [ fxe7;11 = 0g is infeasible, the status of v7 is updated to closed-wrt(fv4g). Next, as the set ILConstraints (v4) [ fxe4;7 = 0g is infeasible, the status of v4 is rst updated to closed-wrt(fv4g) 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 unsatis able. 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 = fa : 9r:9r:(A t fag); a : 3 r:8r::A; a : 8r:B; a : 3 r:B;
r(a; b); b : 8r::A; b : (8r:(:A u :fag) t :B)g; R = ; and T = ;. The rst 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) = ffag; :Ag, applying the rule for dealing with nominals to v13, we delete the edge hv2; v4i (from E) and re-expand v2 by connecting it to new complex non-states v14 and v15 with Label (v14) = Label (v2) [ fa : :Ag and Label (v15) = Label (v2) [ fa : Ag 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 Example 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; frg; ai. The set ILConstraints (v16) consists of xe16;i 0, for 5 i 7, and xe16;5 + xe16;7 xe16;6 + xe16;7 xe16;5 + xe16;6 + xe16;7
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 Example 4.1 when computing Label (v4).
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
Example 4.1 to closed-wrt(fv4g), the statuses of v13, v11, v7 are updated to
closed-wrt(fv17g). Next, as ILConstraints (v17) [ fxe17;7 = 0g is infeasible, the
status of v17 is rst updated to closed-wrt(fv17g) and then updated to closed.
After that, the status of v15 is also updated to closed. As no more changes that
may a ect the status of can be made and Status( ) 6= closed, we conclude that
the knowledge base hR; T ; Ai is satis able. 2
We have presented the rst tableau method with an ExpTime (optimal)
complexity for checking satis ability 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 [
This work di ers from Nguyen's work [