Motivated primarily by medical terminology applications, the prominent DL SHIQ has already been extended to a DL with complex role inclusion axioms of the form R ◦ S v˙ R or S ◦ R v˙ R, called RIQ, and the SHIQ tableau algorithm has been extended to handle such inclusions. This paper further extends RIQ and its tableau algorithm with important expressive means that are frequently requested in ontology applications, namely with reflexive, symmetric, transitive, and irreflexive roles, disjoint roles, and the construct ∃R.Self, allowing, for instance, the definition of concepts such as a “narcist”. Furthermore, we extend the algorithm to cover Abox reasoning extended with negated role assertions. The resulting logic is called SRIQ.
Introduction
– disjoint roles. E.g., the roles sister and mother could be declared as being
disjoint. Most DLs can be said to be “lopsided” since they allow to express
disjointness on concepts but not on roles, despite the fact that role
disjointness is quite natural and can generate new subsumptions or inconsistencies
in the presence of role hierarchies and number restrictions.
– reflexive and irreflexive roles. E.g., the role knows could be declared as being
reflexive, and the role sibling could be declared as being irreflexive. In the
presence of the new concept ∃R.Self described below, reflexive and irreflexive
roles also become definable by Tbox assertions.
– negated role assertions. Most Abox formalisms only allow for positive role
assertions (with few exceptions (1; 5)), whereas SRIQ also allows for
statements such as (John, Mary) : ¬likes. In the presence of complex role
inclusions, negated role assertions can be quite useful and, like disjoint roles, they
overcome a certain “lopsidedness” of DLs.
– Since SRIQ extends SHIQ, we can also express that a role is transitive or
symmetric, and can use role inclusion axioms R v S.
– Since SRIQ extends RIQ (
Besides a Tbox and an Abox, SRIQ provides a so-called Rbox to gather all statements concerning roles.
Secondly, SRIQ is designed to be of similar practicability as SHIQ. The
tableau algorithm for SHIQ and the one for SRIQ presented here are very
similar. Even though the additional expressive means of SRIQ require certain
adjustments to the SHIQ algorithm, these adjustments do not add new sources
of non-determinism, and, subject to empirical verification, are believed to be
“harmless” in the sense of not significantly degrading typical performance as
compared with the SHIQ algorithm. More precisely, we employ the same
technique using finite automata as in (
The current paper describes work in progress towards a description logic
that overcomes certain shortcomings in expressiveness of other DLs. We have
used SHIN , SHIQ, and RIQ as a starting point, extended them with some
“useful-yet-harmless” expressive means, and also extended the tableau algorithm
accordingly. We wish to discuss this extension in case we have overlooked other
“useful-yet-harmless” expressive means, and we plan to further extend SRIQ:
currently, various new operators are restricted to simple roles, and we have yet
to establish which of these restrictions are necessary in order to preserve
decidability1 or practicability. Moreover, we plan to extend SRIQ towards SHOIQ
(
For a full specification of the tableau algorithm and proofs, see (
In this section, we introduce the DL SRIQ. This includes the definition of syntax, semantics, and inference problems. 2.1
Roles, Role Hierarchies, and Role Assertions Definition 1 (Interpretations). Let C be a set of concept names, R a set of role names, and I = {a, b, c . . .} a set of individual names. The set of roles is R ∪ {R− | R ∈ R}, where a role R− is called the inverse role of R.
As usual, an interpretation I = (ΔI , ·I ) consists of a set ΔI , called the domain of I, and a valuation ·I which associates, with each role name R, a binary relation RI ⊆ ΔI ×ΔI , with each concept name C a subset CI ⊆ ΔI and, with each individual name a an element aI ∈ ΔI . Inverse roles are interpreted as usual, i.e., for each role R ∈ R, we have
(R−)I = {hy, xi | hx, yi ∈ RI }.
Note that, unlike in the case of SHIQ, we did not introduce transitive role names. This is so since, as will become apparent below, role box assertions can be used to force roles to be transitive.
To avoid considering roles such as R−−, we define a function Inv on roles such that Inv(R) = R− if R ∈ R is a role name, and Inv(R) = S ∈ R if R = S−.
Since we will often work with a string of roles, it is convenient to extend both ·I and Inv(·) to such strings: if w = R1 . . . Rn for Ri roles, then we set wI = R1I ◦. . .◦RnI and Inv(w) = Inv(Rn) . . . Inv(R1), where ◦ denotes composition of binary relations.
A role box R consists of two components. The first component is a role hierarchy Rh which consists of (generalised) role inclusion axioms, i.e., statements of the form R v˙ S, RS v˙ S, and SR v˙ S. The second component is a set Ra of role assertions stating, for instance, that a role R must be interpreted as a transitive, reflexive, irreflexive, symmetric, or transitive relation, or that two (possibly inverse) roles R and S are to be interpreted as disjoint binary relations.
We start with the definition of a role hierarchy, whose definition involves a strict partial order ≺ on roles, i.e., an irreflexive and transitive relation on R ∪ {R− | R ∈ R}.
Definition 2 ((Regular) Role Inclusion Axioms).
short) is an expression of the form w v˙ R, where w is a finite string of roles,
and R is a role name. A role hierarchy Rh, then, is a finite set of RIAs.
1 See (
S1I ◦ . . . ◦ SnI ⊆ RI , where ◦ stands for the composition of binary relations. An interpretation is a model of a role hierarchy Rh, if it satisfies all RIAs in Rh, written I |= Rh. A RIA w v˙ R is ≺-regular if – R is a role name, – w = RR, – w = R−, – w = S1 . . . Sn and Si ≺ R, for all 1 ≤ i ≤ n, – w = RS1 . . . Sn and Si ≺ R, for all 1 ≤ i ≤ n, or – w = S1 . . . SnR and Si ≺ R, for all 1 ≤ i ≤ n.
Regularity prevents a role hierarchy from containing cyclic dependencies. For instance, the role hierarchy {RS v˙ S,
RT v˙ R,
U T v˙ T,
U S v˙ U }
is not regular because it would require ≺ to satisfy S ≺ U ≺ T ≺ R ≺ S, which
would imply S ≺ S, thus contradicting irreflexivity. Such cyclic dependencies
are known to lead to undecidability (
From the definition of the semantics of inverse roles, it follows immediately that
hx, yi ∈ wI iff hy, xi ∈ Inv(w)I .
Hence, each model satisfying w v˙ S also satisfies Inv(w) v˙ Inv(S) (and vice versa), and thus the restriction to those RIAs with role names on their right hand side does not have any effect on expressivity.
Given a role hierarchy Rh, we define the relation v* to be the transitivereflexive closure of v˙ over {R v˙ S, Inv(R) v˙ Inv(S) | R v˙ S ∈ Rh}. A role R is called a sub-role (resp. super-role) of a role S if R v* S (resp. S v* R). Two roles R and S are equivalent (R ≡ S) if R v* S and S v* R.
Note that, due to the fourth restriction in the definition of ≺-regularity, we also restrict v* to be acyclic, and thus regular role hierarchies never contain two equivalent roles.2
Next, let us turn to the second component of Rboxes, the role assertions. For an interpretation I, we define DiagI to be the set {hx, xi | x ∈ ΔI } and set RI ↓:= {hx, xi | ∃y ∈ ΔI .hx, yi ∈ RI }. 2 This is not a serious restriction for, if R contains v* cycles, we can simply choose one role R from each cycle and replace all other roles in this cycle with R in the input Rbox, Tbox and Abox (see below). Definition 3 (Role Assertions). For roles R and S, we call the assertions Ref(R), Irr(R), Sym(R), Tra(R), and Dis(R, S), role assertions, where, for each interpretation I and all x, y, z ∈ ΔI , we have:
I |= Sym(R) if hx, yi ∈ RI implies hy, xi ∈ RI ; I |= Tra(R) if hx, yi ∈ RI and hy, zi ∈ RI imply hx, zi ∈ RI ; I |= Ref(R) if RI ↓⊆ RI ; I |= Irr(R) if RI ∩ DiagI = ∅; I |= Dis(R, S) if RI ∩ SI = ∅.
Adding symmetric and transitive role assertions is a trivial move since both of these expressive means can be replaced by complex role inclusion axioms as follows: for the role assertion Sym(R) we can add to the Rbox, equivalently, the role inclusion axiom R− v˙ R, and, for the role assertion Tra(R), we can add to the Rbox, equivalently, RR v˙ R. The proof of this should be obvious. Thus, as far as expressivity is concerned, we can assume for convenience that no role assertions of the form Tra(R) or Sym(R) appear in Ra, but that transitive and symmetric roles will be handled by the RIAs alone.
The situation is different, however, for the other Rbox assertions. Neither reflexivity nor irreflexivity nor disjointness of roles can be enforced by role inclusion axioms. However, as we shall see later, reflexivity and irreflexivity of roles are closely related to the new concept ∃R.Self.
In SHIQ, the application of qualified number restrictions has to be restricted
to certain roles, called simple roles, to preserve decidability (
Given a role hierarchy Rh and a set of role assertions Ra (without transitivity or symmetry assertions), the set of roles that are simple in R = Rh ∪ Ra is inductively defined as follows: – a role name is simple if it does not occur on the right hand side of a RIA in
Rh, – an inverse role R− is simple if R is, and – if R occurs on the right hand side of a RIA in Rh, then R is simple if, for each w v˙ R ∈ Rh, w = S for a simple role S.
A set of role assertions Ra is called simple if all roles R, S appearing in role assertions of the form Ref(R), Irr(R), or Dis(R, S) are simple in R. If R is clear from the context, we often use “simple” instead of “simple in R”. Definition 4 (Role Box). A SRIQ-role box (Rbox for short) is a set R =
role assertions.
An interpretation satisfies a role box R (written I |= R) if I |= Rh and I |= φ for all role assertions φ ∈ Ra. Such an interpretation is called a model of R.
Concepts and Inference Problems for SRIQ We are now ready to define the syntax and semantics of SRIQ-concepts. Definition 5 (SRIQ Concepts, Tboxes, and Aboxes). The set of SRIQconcepts is the smallest set such that – every concept name and >, ⊥ are concepts, and, – if C, D are concepts, R is a role (possibly inverse), S is a simple role (possibly inverse), and n is a non-negative integer, then C u D, C t D, ¬C, ∀R.C, ∃R.C, ∃S.Self, (>nS.C), and (6nS.C) are also concepts.
A general concept inclusion axiom (GCI) is an expression of the form
An individual assertion is of one of the following forms: a : C, (a, b) : R, . (a, b) : ¬S, or a 6= b, for a, b ∈ I (the set of individual names), a (possibly inverse) role R, a (possibly inverse) simple role S, and a SRIQ-concept C. A
Note that number restrictions (>nS.C) and (6nS.C), the concept ∃S.Self,
and negated role assertions (a, b) : ¬S, are all restricted to simple roles. In the
case of number restrictions we mentioned the reason for this restriction already:
without it, already the satisfiability problem of SHIQ-concepts is undecidable
(
Note also that, in the definition of SRIQ-Aboxes, we do not assume the
unique name assumption (UNA) (which is commonly assumed in DLs (
Definition 6 (Semantics and Inference Problems).
Given an interpretation I = (ΔI , ·I ), concepts C, D, roles R, S, and nonnegative integers n, the extension of complex concepts is defined inductively by the following equations, where ]M denotes the cardinality of a set M : >I = ΔI , ⊥I = ∅, (¬C)I = ΔI \ CI (top, bottom, negation) (C u D)I = CI ∩ DI , (C t D)I = CI ∪ DI (conjunction, disjunction) (∃R.C)I = {x | ∃y.hx, yi ∈ RI and y ∈ CI } (exists restriction) (∃R.Self)I = {x | hx, xi ∈ RI } (∃R.Self-concepts) (∀R.C)I = {x | ∀y.hx, yi ∈ RI implies y ∈ CI } (value restriction) (>nR.C)I = {x | ]{y.hx, yi ∈ RI and y ∈ CI } > n} (atleast restriction) (6nR.C)I = {x | ]{y.hx, yi ∈ RI and y ∈ CI } 6 n} (atmost restriction)
An interpretation I is a model of a Tbox T (written I |= T ) iff CI ⊆ DI for each GCI C v˙ D in T .
A concept C is called satisfiable iff there is an interpretation I with CI 6= ∅.
each interpretation. Two concepts are equivalent (written C ≡ D) if they are mutually subsuming. The above inference problems can be defined w.r.t. a general role box R and/or a Tbox T in the usual way, i.e., by replacing interpretation with model of R and/or T .
I |= a : C if aI ∈ CI ; I |= (a, b) : R if haI , bI i ∈ RI ; I |= a 6=. b if aI 6= bI ; I |= (a, b) : ¬R if haI , bI i ∈/ RI .
For DLs that are closed under negation, subsumption and (un)satisfiability of concepts can be mutually reduced: C v D iff C u ¬D is unsatisfiable, and C is unsatisfiable iff C v ⊥. Furthermore, a concept C is satisfiable iff the Abox {a : C} is consistent.
It is straightforward to extend these reductions to Rboxes and Tboxes. In contrast, the reduction of inference problems w.r.t. a Tbox to pure concept inference problems (possibly w.r.t. a role hierarchy), deserves special care: in (2; 11; 3), the internalisation of GCIs is introduced, a technique that realises exactly this reduction. For SRIQ, this technique can be modified accordingly.
Now, note also that, instead of having a role assertion Ref(R) ∈ Ra, we can add, equivalently, the GCI ∃R.> v˙ ∃R.Self to T , which can in turn be internalised. Likewise, instead of asserting Irr(R), we can, equivalently, add the GCI > v˙ ¬∃R.Self. Thus, we arrive at the following theorem: Theorem 1. 1. Satisfiability and subsumption of SRIQ-concepts w.r.t. Tboxes and Rboxes are polynomially reducible to (un)satisfiability of SRIQ-concepts w.r.t. Rboxes.
ducible to consistency of SRIQ-Aboxes w.r.t. Rboxes. 3. W.l.o.g., we can assume that Rboxes do not contain role assertions of the form Irr(R), Ref(R), Tra(R), or Sym(R).
With Theorem 1, all standard inference problems for SRIQ-concepts and Aboxes can be reduced to the problem of determining the consistency of a SRIQ-Abox w.r.t. to an Rbox, where we can assume w.l.o.g. that all role assertions in the Rbox are of the form Dis(R, S)—we call such an Rbox reduced.
As we have just seen, we can restrict our attention to the consistency of Aboxes w.r.t. reduced Rboxes only. We have extended the tableau algorithm for RIQ to SRIQ, and will spend the remainder of this paper on its description.
In a first step, the tableau algorithm takes a reduced Rbox R and an Abox A and builds, for each possibly inverse role R occurring in R or A, a nondeterministic finite automaton BR. Intuitively, such an automaton is used to memorise the path between an object x that has to satisfy a concept of the form ∀R.C and other objects, and then to determine which of these objects must satisfy C. The following proposition states that BR indeed captures all implications between (paths of) roles and R that are consequences of the role hierarchy Rh, where L(BR) denotes the language (a set of strings of roles) accepted by BR.
role R occurring in Rh, each word w ∈ L(BR), and each hx, yi ∈ wI , we have hx, yi ∈ RI .
Since Aboxes usually involve several individuals with arbitrary role
relationships between them, the completion algorithm presented works on forests rather
than on trees. A forest is a collection of trees whose root nodes correspond to
the individuals appearing in the input Abox and which form an arbitrarily
connected graph according to the role assertions stated in the Abox. Similar as for
RIQ, we define a set fclos(A, R) of “relevant sub-concepts” of those concepts
occurring in A; see (
a collection of trees whose distinguished root nodes can be connected arbitrarily.
hx, yi from a node x to its successor y is labelled with a non-empty set L(hx, yi) of (possibly inverse and possibly negated) roles occurring in A and R. Finally, completion forests come with an explicit inequality relation 6=. on nodes which is implicitly assumed to be symmetric.
y is called an R-successor of x.
If y is an R-successor of x or x is an Inv(R)-successor of y, then y is called an R-neighbour of x. Moreover, a node x is a neighbour of y, if it is an R-neighbour for some role R. Successors, predecessors, ancestors, and descendants are defined as usual.
For a role S, a concept C, and a node x in F, we define SF(x, C) by
SF(x, C) := {y | y is an S-neighbour of x and C ∈ L(y)}.
A node is blocked iff it is either directly or indirectly blocked. A node x is directly blocked iff none of its ancestors are blocked, and it has ancestors x0, y and y0 such that 1. none of x0, y and y0 is a root node, 2. x is a successor of x0 and y is a successor of y0 and 3. L(x) = L(y) and L(x0) = L(y0) and 4. L(hx0, xi) = L(hy0, yi).
In this case, we say that y blocks x.
A node y is indirectly blocked if one of its ancestors is blocked.
Given a non-empty SRIQ-Abox A and a reduced Rbox R, the tableau algorithm is initialised with the completion forest FA,R defined as follows: – for each individual a occurring in A, FA,R contains a root node xa, – if (a,.b) : R ∈ A or (a, b.) : ¬R ∈ A, then FA,R contains an edge hxa, xbi, – if a 6= b ∈ A, then xa 6= xb is in FA,R, – L(xa) := {C | a : C ∈ A}, and – L(hxa, xbi) := {R | (a, b) : R ∈ A} ∪ {¬R | (a, b) : ¬R ∈ A}.
A completion forest F is said to contain a clash if there are nodes x and y such that 1. ⊥ ∈ L(x), or 2. for some concept name A, {A, ¬A} ⊆ L(x), or
6. there is some concept (6nS.C) ∈ L(x) and {y0, . . . , yn} ⊆ SF(x, C) with .
yi 6= yj for all 0 ≤ i < j ≤ n.
A completion forest that does not contain a clash is called clash-free. A completion forest is complete if none of the rules from Figure 1 can be applied to it.
leau algorithm initialises FA,R and repeatedly applies the expansion rules from Figure 1 to it, stopping when a clash occurs, and applying the shrinking rules eagerly, i.e., the ≤- and the ≤r-rule are applied with highest priority. The algorithm answers “A is satisfiable w.r.t. R” iff the expansion rules can be applied in such a way that they yield a complete and clash-free completion forest, and “A is unsatisfiable w.r.t. R” otherwise.
form and R a reduced Rbox.
– The tableau algorithm terminates when started for A and R. – The expansion rules can be applied to A and R such that they yield a complete and clash-free completion forest iff there is a tableau for A w.r.t. R.
From Theorem 1 and Lemma 1, we thus have the following theorem: Theorem 2. The tableau algorithm decides satisfiability and subsumption of SRIQ-concepts with respect to Aboxes, Rboxes, and Tboxes. u-rule: if C1 u C2 ∈ L(x), x is not indirectly blocked, and {C1, C2} 6⊆ L(x), then L(x) −→ L(x) ∪ {C1, C2} t-rule: if C1 t C2 ∈ L(x), x is not indirectly blocked, and
{C1, C2} ∩ L(x) = ∅ then L(x) −→ L(x) ∪ {E} for some E ∈ {C1, C2} ∃-rule: if ∃S.C ∈ L(x), x is not blocked, and
x has no S-neighbour y with C ∈ L(y) then create a new node y with
L(hx, yi) := {S} and L(y) := {C} Self-rule: if ∃S.Self ∈ L(x), x is not blocked, and S ∈/ L(hx, xi) then add an edge hx, xi if it does not yet exist, and
set L(hx, xi) −→ L(hx, xi) ∪ {S} ∀1-rule: if ∀S.C ∈ L(x), x is not indirectly blocked, and
∀BS.C 6∈ L(x) then L(x) −→ L(x) ∪ {∀BS.C} ∀2-rule: if ∀B(p).C ∈ L(x), x is not indirectly blocked, p →S q in B(p), and there is an S-neighbour y of x with ∀B(q).C ∈/ L(y), then L(y) −→ L(y) ∪ {∀B(q).C} ∀3-rule: if ∀B.C ∈ L(x), x is not indirectly blocked, ε ∈ L(B), and C 6∈ L(x) then L(x) −→ L(x) ∪ {C} choose-rule: if (6nS.C) ∈ L(x), x is not indirectly blocked, and
there is an S-neighbour y of x with {C, ¬˙C} ∩ L(y) = ∅ then L(y) −→ L(y) ∪ {E} for some E ∈ {C, ¬˙C} >-rule: if (>nS.C) ∈ L(x), x is not blocked, and there are no y1, . . . , yn ∈ SF(x, C)
.
with yi 6= yj for each 1 ≤ i < j ≤ n then create n new successors y1, . . . , yn of x with L(hx, yii) = {S},
.
L(yi) = {C}, and yi 6= yj for 1 ≤ i < j ≤ n. 6-rule: if (6nS.C) ∈ L(x), x is not indirectly blocked, and #SF(x, C) > n, there are y, z ∈ SF(x, C) with
.
not y 6= z and y is not a root node nor an ancestor of z, then 1. L(z) −→ L(z) ∪ L(y) and 2. if z is an ancestor of x then L(hz, xi) −→ L(hz, xi) ∪ Inv(L(hx, yi)) else L. (hx, zi) −→ L(hx, zi) ∪ L(hx, yi)
. 3. Set u 6= z for all u with u 6= y.
4. remove y and the sub-tree below y from F. 6r-rule: if (6nS.C) ∈ L(x), #SF(x, C) > n, .
and there are two root nodes y, z ∈ SF(x, C) with not y 6= z, then 1. L(z) −→ L(z) ∪ L(y) and 2. For all edges hy, wi: i. if the edge hz, wi does not exist, create it with L(hz, wi) := L(hy, wi); ii. else L(hz, wi) −→ L(hz, wi) ∪ L(hy, wi). 3. For all edges hw, yi: i. if the edge hw, zi does not exist, create it with L(hw, zi) := L(hw, yi); ii. else. L(hw, zi) −→ L(hw., zi) ∪ L(hw, yi). 4. Set u 6= z for all u with u 6= y.
5. Remove y and all incoming and outgoing edges from y from F.
Fig. 1. The Expansion Rules for the SRIQ Tableau Algorithm.