=Paper=
{{Paper
|id=None
|storemode=property
|title=An ExpTime Tableau Method for Dealing with Nominals and Quantified Number Restrictions
in Deciding the Description Logic SHOQ
|pdfUrl=https://ceur-ws.org/Vol-1032/paper-26.pdf
|volume=Vol-1032
|dblpUrl=https://dblp.org/rec/conf/csp/NguyenG13
}}
==An ExpTime Tableau Method for Dealing with Nominals and Quantified Number Restrictions
in Deciding the Description Logic SHOQ==
https://ceur-ws.org/Vol-1032/paper-26.pdf
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/.