We present a decidable extension of the Description Logic SROIQ that supports defeasible reasoning in the KLM tradition, and extends it through the introduction of defeasible roles. The semantics of the resulting DL dSROIQ extends the classical semantics with a parameterised preference order on binary relations in a domain of interpretation. This allows for the use of defeasible roles in complex concepts, as well as in defeasible concept and role subsumption, and in defeasible role assertions. Reasoning over dSROIQ ontologies is made possible by a translation of entailment to concept satisfiability relative to an RBox only. A tableau algorithm then decides on consistency of dSROIQ-concepts in the preferential semantics.
Introduction
SROIQ [
Given the special status of subsumption in DLs in particular, and the historical importance of entailment in logic in general, past research efforts in this direction have focused primarily on accounts of defeasible subsumption and the characterisation of defeasible entailment. Semantically, the latter usually take as point of departure orderings on a class of first-order interpretations, whereas the former usually assume a preference order on objects of the domain.
In this paper, we propose a decidable extension of SROIQ that supports defeasible
knowledge representation and reasoning over defeasible ontologies. Our proposal builds
on previous work to resolve two important ontological limitations of the preferential
approach to defeasible reasoning in DLs — the assumption of a single preference order
on all objects in the domain of interpretation, and the assumption that defeasibility is
intrinsically linked to argument form [
We achieve this by extending SROIQ with nonmonotonic reasoning features in the concept language, in subsumption statements and in role assertions via an intuitive notion of normality for roles. This parameterises the idea of preference while at the same time introducing the notion of defeasible class membership. Defeasible subsumption allows for the expression of statements of the form “C is usually subsumed by D”, for example, “Chenin blanc wines are usually unwooded”. In our extended language dSROIQ, we can now also refer directly to, for example, “Chenin blanc wines that usually have a wood aroma”. We can also combine these seamlessly, as in: “Chenin blanc wines that usually have a wood aroma are usually wooded”. Note that this cannot be expressed in terms of defeasible subsumption alone, nor can it be expressed w.l.o.g. using a typicality operator on concepts. This is because the semantics of the expression is inextricably tied to the two distinct uses of the term ‘usually’. Another defeasible construct that adds to the expressivity of dSROIQ is defeasible role inclusion, e.g. “having a given geographic style usually implies having that region as origin”. dSROIQ also includes defeasible role assertions, such as defeasible functionality or defeasible disjointness, and defeasible number- and Self-restrictions.
The remainder of the paper is structured as follows: In Section 2 we introduce the syntax and semantics of the extended language dSROIQ. Section 3 covers a number of rewriting and elimination results required for effective reasoning with dSROIQ knowledge bases, and which are needed for the tableau algorithm presented in Section 4. The main results of the paper are Theorem 1, which reduces concept satisfiability in dSROIQ to concept satisfiability relative to only an RBox, and Theorem 2, which establishes the correctness of the tableau procedure. The latter result is established only for the restriction of dSROIQ which excludes role composition in defeasible RIAs.
Space considerations prevent us from providing a summary of the required
logical background. We shall therefore assume the reader’s familiarity with DLs in
general [
Let R be a set of role names, and let u denote the universal role. The set of all roles is given by R := R [ fr j r 2 Rg [ fug. We denote roles with r; s; : : :, possibly with subscripts. Moreover, let inv : R ! R be such that inv : r 7! r , if r 2 R, inv : r 7! s, if r = s , and inv : u 7! u.
Let r1; : : : ; rn; r 2 R n fug. A classical role inclusion axiom is a statement of the form r1 rn v r. A defeasible role inclusion axiom has the form r1 rn @ r, read “usually, r1 rn is included in r”. A finite set of role inclusion axioms (RIAs) is called a role hierarchy and is denoted by Rh.
Definition 1 ((Non-)Simple Role). Let r 2 R and let Rh be a role hierarchy. Then r is non-simple in Rh iff: 1. There is r1 rn v r or r1 rn @ r in Rh such that n > 1, or 2. There is s v r or s @ r in Rh such that s is non-simple, or
With Rn we denote the set of non-simple roles in Rh. Rs := R n Rn is the set of simple roles in Rh.
Intuitively, simple roles are those that are not implied by the composition of roles.
They are needed to restrict the type of roles in certain concept constructors (see below),
thereby preserving decidability [
Definition 2 (Regular Hierarchy). A role hierarchy Rh is regular if there is a strict partial order < on Rn such that: 1. s < r iff inv(s) < r, for every r; s in Rn, and 2. every role inclusion in Rh is of one of the forms: (1a) r r v r, (1b) r r @ r, (2a) inv(r) v r, (2b) inv(r) @ r, (3a) s1 sn v r, (3b) s1 sn @ r, (4a) r s1 sn v r, (4b) r s1 sn @ r, (5a) s1 sn r v r, (5b) s1 sn r @r, where r 2 R (i.e., a role name), and si < r, for i = 1; : : : ; n. (Regularity prevents a role hierarchy from inducing cyclic dependencies, which are known to lead to undecidability.)
A classical role assertion is a statement of the form Fun(r) (functionality), Ref(r) (reflexivity), Irr(r) (irreflexivity), Sym(r) (symmetry), Asy(r) (asymmetry), Tra(r) (transitivity), and Dis(r; s) (role disjointness), where r; s 6= u. A defeasible role assertion is a statement of the form dFun(r) (r is usually functional), dRef(r) (r is usually reflexive), dIrr(r) (r is usually irreflexive), dSym(r) (r is usually symmetric), dAsy(r) (r is usually asymmetric), dTra(r) (r is usually transitive), and dDis(r; s) (r and s are usually disjoint), also with r; s 6= u. With Ra we denote a finite set of role assertions.
Given a role hierarchy Rh, we say that Ra is simple w.r.t. Rh if all roles r; s appearing in statements of the form Irr(r), dIrr(r), Asy(r), dAsy(r), Dis(r; s) or dDis(r; s) are simple in Rh (see Definition 1).
A dSROIQ RBox is a set R := Rh [ Ra, where Rh is a regular hierarchy and Ra is a set of role assertions which is simple w.r.t. Rh. 2.2
Let C be a set of (atomic) concept names disjoint from R and of which N, the set of nominals, is a subset. We use A; B; : : :, possibly with subscripts, to denote concept names. A nominal will also be denoted by o, possibly with subscripts. Definition 3 (dSROIQ Concepts). The set of dSROIQ complex concepts is the smallest set such that >, ? and every A 2 C are concepts, and if C and D are concepts, r 2 R, s 2 Rs, and n 2 N, then :C (concept complement), C u D (concept conjunction), C t D (concept disjunction), 8r:C (value restriction), 9r:C (existential restriction), Wr:C (defeasible value restriction), jr:C (defeasible existential restriction), 9r:Self (self restriction), jr:Self (defeasible self restriction), ns:C (at-least restriction), ns:C (at-most restriction), & ns:C (defeasible at-least restriction), . ns:C (defeasible at-most restriction) are also concepts. With C we denote the set of all complex concepts.
Note that every SROIQ concept is a dSROIQ concept, too. We shall use C; D : : :, possibly with subscripts, to denote complex dSROIQ concepts.
Given C; D 2 C, C v D is a classical general concept inclusion, read “C is subsumed by D”. (C D is an abbreviation for both C v D and D v C.) C @ D is a defeasible general concept inclusion, read “C is usually subsumed by D”. A dSROIQ TBox T is a finite set of general concept inclusions (GCIs), whether classical or defeasible.
Let I be a set of individual names disjoint from both C and R. Given C 2 C, r 2 R and a; b 2 I, an individual assertion is an expression of the form a : C, (a; b) : r, (a; b) : :r, a = b or a 6= b. A dSROIQ ABox A is a finite set of individual assertions.
Let A be an ABox, T be a TBox and R an RBox. A knowledge base (alias ontology) is a tuple KB := hA; R; T i. 2.3
We shall anchor our semantic constructions in the well-known preferential approach to
non-monotonic reasoning [
Let X be a set and let < be a strict partial order on X. With min< X := fx 2 X j there is no y 2 X s.t. y < xg we denote the minimal elements of X w.r.t. <. With #X we shall denote the cardinality of X.
Definition 4 (Ordered Interpretation). An ordered interpretation is a tuple O :=
h O; O; O; Oi in which h O; Oi is a SROIQ interpretation with AO O,
for every A 2 C, AO a singleton for every A 2 N, rO O O, for all r 2 R,
and aO 2 O, for every a 2 I, O is a strict partial order on O, and O:=
h 1O; : : : ; O#Ri, where iO riO riO, for i = 1; : : : ; #R, and such that O and
each iO satisfy the smoothness condition [
O; ?O := ;; (:C)O :=
O n CO; (C u D)O := CO \ DO; (8r:C)O := fx j rO(x)
(C t D)O := CO [ DO; COg; (Wr:C)O := fx j min O (rOjx)(x) COg; (9r:C)O := fx j rO(x) \ CO 6= ;g; ( jr:C)O := fx j min O (rOjx)(x) \ CO 6= ;g; nr:C)O := fx j #rO(x) \ CO (9r:Self)O := fx j (x; x) 2 rOg; ( jr:Self)O := fx j (x; x) 2 min O (rOjx)g; ( nr:C)O := fx j #rO(x) \ CO ng; ( ng; (& nr:C)O := fx j # min O (rOjx)(x) \ COg (. nr:C)O := fx j # min O (rOjx)(x) \ CO n; ng:
It is not hard to see that, analogously to the classical case, W and j, as well as & and ., are duals to each other.
Definition 5 (Satisfaction). Let O = h C; D 2 C, and a; b 2 I. The satisfaction relation
O; O; O;
Oi and let r1; : : : ; rn; r; s 2 R, is defined as follows: O r v s if rO sO; O r @ s if min O rO sO; O r1 rn v r if (r1 rn)O rO; O r1 rn @ r if min O (r1 rn)O rO; O Fun(r) if rO is a function; O dFun(r) if for all x, # min O (rOjx)(x) 1; O Ref(r) if f(x; x) j x 2 Og rO; O dRef(r) if for every x 2 min O O, (x; x) 2 rO; O Irr(r) if rO \ f(x; x) j x 2 Og = ;; O dIrr(r) if for every x 2 min O O, (x; x) 2= rO; O Sym(r) if inv(r)O rO; O dSym(r) if min O (r )O rO; O Asy(r) if rO \ inv(r)O = ;; O dAsy(r) if min O rO \ min O (r )O = ;; O Tra(r) if (r r)O rO; O dTra(r) if min O (r r)O rO; O Dis(r; s) if rO \ sO = ;; O dDis(r; s) if min O rO \ min O sO = ;; O C v D if CO DO; O C @ D if min O CO DO; O a : C if aO 2 CO; O (a; b) : r if (aO; bO) 2 rO; O (a; b) : :r if O 6 (a; b) : r; O a = b if aO = bO; O a 6= b if O 6 a = b.
If O , then we say O satisfies . O satisfies a set of statements or assertions X (denoted O X) if O for every 2 X, in which case we say O is a model of X. We say C 2 C is satisfiable w.r.t. KB = hA; R; T i if there is a model O of KB s.t. CO 6= ;, and unsatisfiable otherwise.
A statement is (classically) entailed by a knowledge base KB, denoted KB j= , if every model of KB satisfies . 3
As for classical SROIQ [20, Lemma 7], it is possible to eliminate an ABox A by compiling all individual assertions in A as follows: 1. Let N0 := N [ foa j a appears in Ag (i.e., extend the signature with new nominals); 2. Let A0 := fa : C 2 Ag [ fa : 9r:ob j (a; b) : r 2 Ag [ fa : 8r::ob j (a; b) : :r 2
Ag [ fa : :ob j a 6= b 2 Ag; 3. For every C 2 C, let C0 := C u da:D2A0 9u:(oa u D).
It is then easy to see that C is satisfiable w.r.t. hA; R; T i if and only if C0 is satisfiable w.r.t. h;; R; T i, which allows us to assume from now on and w.l.o.g. that ABoxes have been eliminated.
Next, in the same way that most of the classical role assertions can equivalently be replaced by GCIs or RIAs, under our preferential semantics, all of our defeasible role assertions, with the exception of dAsy( ) and dDis( ), can be reduced to defeasible RIAs in the following way. dFun(r) can be replaced by > v. 1r:> — to be ‘usually functional’ means only non-normal arrows can break functionality. (Note that, since the number restriction is unqualified, r need not be simple.) dRef(r) and dIrr(r) can, respectively, be replaced with > @ 9r:Self and > @ :9r:Self. dSym(r) can be reduced to r @ r and dTra(r) to r r @ r. Furthermore, note that dAsy(r) can be reduced to dDis(r; r ) (cf. Definition 5). Hence, from now on we can assume, w.l.o.g., that the set of role assertions Ra contains only statements of the form Dis(r; s) and dDis(r; s).
Next, we observe that defeasible concept inclusions can be made classical by
introducing a new role name r to encode at the object level. This is similar to the
SROIQ encoding of the typicality operator of Giordano et al. [
Finally, we can apply the same procedure for eliminating both the TBox and the
universal role u defined for classical SROIQ [20, Lemma 8][
The next theorem summarises the reduction outlined in this section: Theorem 1. Satisfiability of dSROIQ-concepts w.r.t. TBoxes, ABoxes and RBoxes can be polynomially reduced to satisfiability of dSROIQ-concepts w.r.t. RBoxes in which all role assertions are of the form Dis(r; s) and dDis(r; s).
It is known that classical RIAs with role composition on the LHS can be eliminated
via automata-based procedures [
Furthermore, note that the special role name r used in the internalisation of defeasible concept inclusions does not appear in W-, j-, &- or .-concepts or in defeasible RIAs, for r 2= R. 4
We shall now present a tableau-based algorithm for deciding consistency of dSROIQconcepts w.r.t. an RBox. Thanks to the results in Section 3, it also allows for checking concept satisfiability w.r.t. knowledge bases KB = hA; R; T i.
The algorithm extends that for SROIQ [
With nnf(C) we denote the negation normal form (NNF) of C 2 C, i.e., the result of transforming C into an equivalent concept by pushing negation inwards and applying De Morgan’s laws as well as the duality between 8 and 9, and , W and j, and & and .. Note that in NNF negation occurs only in front of concept names or in front of 9r:Self or jr:Self.
If C 2 C, sub(C) denotes the set of all (syntactic) sub-concepts of C (including C itself), and clos(C) is the smallest set containing C that is closed under sub-concepts and negation: clos(C) := fD j D 2 sub(C)g [ fnnf(:D) j D 2 sub(C)g. Definition 6 (Completion Graph). Let C 2 C be in NNF and such that the universal role u does not occur in C, and let R be an RBox. A completion graph for C w.r.t. R is a directed graph G := hV; E; M; L; N ; 6 =:i where V is a set of nodes, E V V is a set of edges, M E E is a relation on edges, L( ) is a labelling function defined by: nr:D 2 clos(C) and V
N 1. for every v 2 V , L(v) clos(C) [ N [ f
m ng [ f. mr:D j . nr:D 2 clos(C) and m 2. for every e = (v; v0) 2 E, L(e) R n fug; 3. for every m = (e; e0) 2 M , L(m) L(e) \ L(e0),
E R, with (e; r) 2 N only if r 2 L(e), and 6=: mr:D j ng; Intuitively, N tells us whether (v; v0) is a normal r-edge among those leaving v. It is used along with M in the model-unravelling phase to construct a preference relation for each role name. (For the sake of readability, we shall henceforth write L(v; v0) and L((v; v0); (u; u0)) instead of L((v; v0)) and L(((v; v0); (u; u0))).) M is the explicit construction of the skeleton of the preference relation on the edges, and is used to construct the model resulting from the unravelling of the completion graph.
If (v; v0) 2 E, then v0 is a successor of v, and v is a predecessor of v0. Ancestor is the transitive closure of predecessor, and descendant is the transitive closure of successor. We say v0 is an r-successor of v if r 2 L(v; v0). v is an r-predecessor of v0 if v0 is an r-successor of v. Neighbour (resp. r-neighbour) is the union of successor (resp. r-successor) and predecessor (r-predecessor). If r 2 R n fug, C 2 C and v 2 V in G, then
rG (v; C) := fv0 j (v; v0) 2 E; r 2 L(v; v0); and C 2 L(v0)g denotes all r-successors of v with C in their label, and rG (v; C) := rG (v; C) \ fv0 j ((v; v0); r) 2 N g
N denotes (intuitively) the r-successors of v with C in their label that are accessible via an r-edge which is minimal among r-edges leaving v. : Definition 7 (Clash). Let G = hV; E; M; L; N ; 6=i be a completion graph. We say G contains a clash if there are nodes v; v0; v00; v1; : : : ; vk; v10; : : : ; vk0 2 V such that: 1. ? 2 L(v), or for some A 2 C, fA; :Ag L(v); 2. r 2 L(v; v) and :9r:Self 2 L(v); 3. r 2 L(v; v), ((v; v); r) 2 N and : jr:Self 2 L(v); 4. Dis(r; s) 2 Ra, (v; v0) 2 E and fr; sg L(v; v0); 65.. dDnisr(:rC; s2) 2L(Rv)a,a(nvd; fvv0)0;2: :E: ;, vfnr;gsg rGL(v(;vC;v)0,)wahnedre((vvi; 6=v:0)v;jr)fo;(r(0v; v0i);<s)j2 Nn;; : 7. . nr:C 2 L(v) and fv0; : : : ; vng rNG (v; C), where vi 6= vj for 0 8. ((v; v0); r) 2 N and r 2 L((v; v00); (v; v0)); 9. r 2 L((vi; vi0); (vi+:1; vi0+1)), for i = 1; : : : ; k 10. for some o 2 N, v 6= v0 and o 2 L(v) \ L(v0). 1, and vk = v1, vk0 = v10, or i < j n;
In order to ensure termination of the algorithm in the presence of transitive roles,
we extend the standard (classical) blocking technique [
If (1)–(5) hold, we say u blocks v. We say v 2 V is blocked if either (a) v is label blocked, or (b) v is blockable and there is (v0; v) 2 E such that v0 is blocked. If v is blocked but is not label blocked, then we say v is indirectly blocked.
Let C be the concept of which the satisfiability w.r.t. an RBox R one wants to check, and let o1; : : : ; ok be the nominals occurring in C. The tableau algorithm is initialised with a completion graph G = hfv0; v1; : : : ; vkg; ;; ;; L; ;; ;i, where L(v0) := fCg, L(vi) := foig, for 1 i k. We then expand G by decomposing concepts in its nodes through the application of the expansion rules in Figures 1–3. These rules are repeatedly applied until either no more rules are applicable or a clash (Definition 7) is found. In either case, we say the completion graph is complete. The algorithm returns “C is satisfiable w.r.t. R”, if the result of the application of the expansion rules to C and R is a complete and clash-free graph, and “C is unsatisfiable w.r.t. R”, otherwise.
Note that the rules in Figure 1 are the same as the corresponding ones for SROIQ modulo the new definitions of blocking (see Definition 8), and of merging and pruning (see below). The rules in Figure 3 deal specifically with our new non-monotonic constructs. The rules in Figure 2 correspond to those classical rules that had to be modified in the light of our richer semantics. We here detail the case of the 9-rule, from which the respective explanations for the Self-, - and NN-rules can be constructed. Unlike in the j-rule, we cannot assume the newly added r-edge is minimal among r-successors of v. We therefore need to consider the additional possibility that the new r-edge is not normal. (This has to be dealt with explicitly in order to ensure soundness of the algorithm.) Therefore, when creating a new r-successor, there are two possibilities: either (i) the new edge is normal among the r-edges leaving v, in which case the result is the u-rule: if then t-rule: if then 8-rule: if then ch-rule: if then -rule: if o-rule: if then C1 u C2 2 L(v), v is not indirectly blocked, and fC1; C2g 6 L(v) L(v) := L(v) [ fC1; C2g C1 t C2 2 L(v), v is not indirectly blocked, fC1; C2g \ L(v) = ; L(v) := L(v) [ fC0g, for some C0 2 fC1; C2g 8r:C 2 L(v), v is not indirectly blocked, r 2 L(v; v0), C 2= L(v0) L(v0) := L(v0) [ fCg
nr:C 2 L(v), v is not indirectly blocked, r 2 L(v; v0), and fC; nnf(:C)g \ L(v0) = ; L(v0) := L(v0) [ fC0g, for some C0 2 fC; nnf(:C)g
nr:C 2 L(v), v is not indirectly blocked, #rG(v; C) > n, and there are v1; v2 s.t. r 2 L(v; v1) \ L(v; v2), C 2 L(v1) \ L(v2); but not v1 6 =: v2 then a. if v1 is a nominal node, then merge(v2; v1), b. else if v2 is a nominal node or an ancestor of v1, then merge(v1; v2) c. else merge(v2; v1) for some o 2 N there are v; v0 s.t. o 2 L(v) \ L(v0) and not v 6 =: v0 merge(v; v0) same as that of applying the j-rule, or (ii) it is not normal, in which case there must be a most preferred r-edge, which is also more preferred than the newly created one. (This splitting is of the same nature as that in the t-rule, fitting the purpose of a proof by cases.) The additional index k in the - and NN-rules serve a similar purpose. :
The result of prune(v) in G = hV; E; M; L; N ; 6=i is a new completion graph constructed from G as follows: (1) For every successor v0 of v, E := E n f(v; v0)g and if v0 is blockable, then prune(v0); (2) V := V n fvg. (We assume these changes are : propagated to L, M , N and 6= in the expected way.) :
The result of merge(v0; v) in G = hV; E; M; L; N ; 6=i is a new completion graph constructed from G in the following way (conditions (d)–(f) in both clauses (1) and (2) below are used to preserve the relative normality of the edges): 1. For every u s.t. (u; v0) 2 E: (a) if f(v; u); (u; v)g \ E = ;, then E := E [ f(u; v)g and L(u; v) := L(u; v0); (b) if (u; v) 2 E, then L(u; v) := L(u; v) [ L(u; v0); (c) if (v; u) 2 E, then L(v; u) := L(v; u) [ finv(r) j r 2 L(u; v0)g; (d) if (x; y) 2 E and ((x; y); (u; v0)) 2 M , then M := M n f((x; y); (u; v0))g [ f((x; y); (u; v))g and L((x; y); (u; v)) := L((x; y); (u; v))[L((x; y); (u; v0)); (e) if (x; y) 2 E and ((u; v0); (x; y)) 2 M , then M := M n f((u; v0); (x; y))g [ f((u; v); (x; y))g and L((u; v); (x; y)) := L((u; v); (x; y))[L((u; v0); (x; y)); (f) if ((u; v0); r) 2 N , then N := N [ f((u; v); r)g; (g) E := E n f(u; v0)g; 2. For every nominal node u s.t. (v0; u) 2 E: (a) if f(v; u); (u; v)g \ E = ;, then E := E [ f(v; u)g and L(v; u) := L(v0; u); (b) if (v; u) 2 E, then L(v; u) := L(v; u) [ L(v0; u); (c) if (u; v) 2 E, then L(u; v) := L(u; v) [ finv(r) j r 2 L(v0; u)g;
if 9r:C 2 L(v), v is not blocked, and there is no v0 s.t. r 2 L(v; v0) and C 2 L(v0) then 1. create a new node v0 and edge (v; v0) with L(v0) := fCg, L(v; v0) := frg and N := N [ f((v; v0); r)g or 2. create two new nodes v0; v00 and new edges (v; v0), (v; v00) with L(v0) := fCg, L(v; v0) := frg,
M := M [ f((v; v00); (v; v0))g, L((v; v00); (v; v0)) := frg and N := N [ f((v; v00); r)g Self-rule: if 9r:Self 2 L(v), v is not blocked, and r 2= L(v; v) then 1. add an edge (v; v), if it does not exist, L(v; v) := L(v; v) [ frg, and N := N [ f((v; v); r)g or 2. create a node v0 and edges (v; v), (v; v0), L(v; v) := L(v; v) [ frg, L(v; v0) := frg,
M := M [ f((v; v0); (v; v))g, L((v; v0); (v; v)) := frg, and N := N [ f((v; v0); r)g -rule: if
nr:C 2 L(v), v is not blocked, and there are no v1; : : : ; vn s.t. r 2 L(v; vi), C 2 L(vi), i = 1; : : : ; n, and vi 6 =: vj , for 1 i < j n, and each vi is not blocked if v is not blockable then a. guess k 2 f0; : : : ; ng, b. create k new nodes v1; : : : ; vk and edges (v; vi), for i = 1; : : : ; k, with L(v; vi) := frg,
L(vi) := fCg and N := N [ f((v; vi); r)g, c. create 2(n k) new nodes vk+1; : : : ; vn and vk0+1; : : : ; vn0 and edges (v; vi) and (v; vi0), for i = k + 1; : : : ; n, with L(vi) := fCg, L(v; vi) := frg, L(v; vi0) := frg,
M := M [ f((v; vi0); (v; vi))g, L((v; vi0); (v; vi)) := frg and N := N [ f((v; vi0); r)g, and d. set vi 6 =: vj , for 1 i < j n NN-rule: if 1. nr:C 2 L(v), v is not blockable, r 2 L(v0; v), v0 is blockable, and C 2 L(v0) 2. there is no m 2 f1; : : : ; ng s.t. mr:C 2 L(v) and s.t. there are m nominal r-successors
v1; : : : ; vm of v with C 2 L(vi) and vi 6 =: vj for all 1 i < j m then a. guess m 2 f1; : : : ; ng, set L(v) := L(v) [ f. mr:Cg and guess k 2 f0; : : : ; mg, b. create k new nodes v1; : : : ; vk and edges (v; vi), for i = 1; : : : ; k, with L(v; vi) := frg,
L(vi) := fC; oig with each oi 2 N new in G and N := N [ f((v; vi); r)g, c. create 2(m k) new nodes vk+1; : : : ; vm and vk0+1; : : : ; vm0 and edges (v; vi) and (v; vi0), for i = k + 1; : : : ; m, with L(v; vi) := f g
r , L(vi) := fC; oig, with each oi 2 N new in G, L(v; vi0) := frg,
M := M [ f((v; vi0); (v; vi))g, L((v; vi0); (v; vi)) := frg and N := N [ f((v; vi0); r)g, and d. set vi 6 =: vj , for 1 i < j m
(d) if (x; y) 2 E and ((x; y); (v0; u)) 2 M , then M := M n f((x; y); (v0; u))g [ f((x; y); (v; u))g and L((x; y); (v; u)) := L((x; y); (v; u))[L((x; y); (v0; u)); (e) if (x; y) 2 E and ((v0; u); (x; y)) 2 M , then M := M n f((v0; u); (x; y))g [ f((v; u); (x; y))g and L((v; u); (x; y)) := L((v; u); (x; y))[L((v0; u); (x; y)); (f) if ((v0; u); r) 2 N , then N := N [ f((v; u); r)g; (g) E := E n f(v0; u)g;
As in the classical case, in order to ensure termination of the tableau algorithm, one has to assign higher priorities to certain rules. Here we assume the following strategy is adopted: The o-rule is applied with the highest priority; the NN- and dNN-rules are applied before the - and .-rules; the other rules are applied with a lower priority. Theorem 2. Let C 2 C and let R be an RBox. 1. The algorithm terminates if started with nnf (C ) and R; 2. When exhaustively applied to nnf (C ) and R, the expansion rules yield a complete and clash-free completion graph iff C is satisfiable w.r.t. R. r 2 L(v; v0), v is not indirectly blocked and either r v s 2 R or both r @ s 2 R and ((v; v0); r) 2 N L(v; v0) := L(v; v0) [ fsg jr:C 2 L(v), v is not blocked and there is no v0 s.t. r 2 L(v; v0), C 2 L(v0) and ((v; v0); r) 2 N create a new node v0 and edge (v; v0) with L(v0) := fCg, L(v; v0) := frg and N := N [ f((v; v0); r)g jr:Self 2 L(v), v is not blocked and either r 2= L(v; v) or ((v; v); r) 2= N add a new edge (v; v), if required, L(v; v) := L(v; v) [ frg, and N := N [ f((v; v); r)g Wr:C 2 L(v), v is not indirectly blocked, r 2 L(v; v0), ((v; v0); r) 2 N and C 2= L(v0) L(v0) := L(v0) [ fCg . nr:C 2 L(v), v is not indirectly blocked, r 2 L(v; v0), ((v; v0); r) 2 N and fC; nnf(:C)g \ L(v0) = ; L(v0) := L(v0) [ fC0g, for some C0 2 fC; nnf(:C)g & nr:C 2 L(v), v is not blocked, and there are no v1; : : : ; vn s.t. r 2 L(v; vi), ((v; vi); r) 2 N , C 2 L(vi), for i = 1; : : : ; n, and s.t. vi 6 =: vj , for 1 i < j n, and each vi is not blocked if v is not blockable create n new nodes v1; : : : ; vn with L(v; vi) = frg, N := N [ f((v; vi); r)g, L(vi) = fCg, for i = 1; : : : ; n, and set vi 6 =: vj , 1 i < j n . nr:C 2 L(v), v is not indirectly blocked, #rNG (v; C) > n, and there are v1; v2 s.t. : r 2 L(v; v1) \ L(v; v2), ((v; v1); r); ((v; v2); r) 2 N , C 2 L(v1) \ L(v2) but not v1 6= v2 then a. if v1 is a nominal node, then merge(v2; v1), else b. if v2 is a nominal node or an ancestor of v1, then merge(v1; v2) c. else merge(v2; v1) dNN-rule: if 1. . nr:C 2 L(v), v is not blockable, r 2 L(v0; v), v0 is blockable and C 2 L(v0) 2. there is no m 2 f1; : : : ; ng s.t. . mr:C 2 L(v) and s.t. there are m nominal nodes v1; :: : : ; vm with (v; vi) 2 E, r 2 L(v; vi), ((v; vi); r) 2 N , C 2 L(vi), for i = 1; : : : ; m, and with vi 6= vj , for all 1 i < j m then a. guess m 2 f1; : : : ; ng and set L(v) := L(v) [ f. mr:Cg b. create m new nodes v10; : : : ; vm0 with L(v; vi0) := frg, N := N [ f:((v; vi0); r) j 1 i ng,
L(vi0) := fC; oig, with oi 2 N new in G, i = 1; : : : ; m, and set vi0 6= vj0 , 1 i < j m The main contributions of the present paper are: (i) a meaningful extension of S ROI Q with defeasible reasoning constructs in the concept language, in both concept and role inclusions, and in role assertions, together with an intuitive KLM-style preferential semantics; (ii) a translation of the entailment problem w.r.t. dS ROI Q knowledge bases to concept satisfiability relative to an RBox only, and (iii) a terminating, sound and complete tableau-based algorithm for checking concept satisfiability w.r.t. dS ROI Q RBoxes.
As for the next steps, we have (i) extending the tableau procedure to allow role composition in defeasible RIAs, (ii) an analysis of the computational complexity of concept satisfiability for dS ROI Q, (iii) an investigation of the correspondence between dS ROI Q and an extension of the OWL 2 RDF semantics3, and (iv) the definition of an appropriate notion of non-monotonic entailment for dS ROI Q ontologies. 3 https://www.w3.org/TR/2012/REC-owl2-rdf-based-semantics-20121211