Axiom weakening is a technique that allows for a ne-grained repair of inconsistent ontologies. Its main advantage is that it repairs ontologies by making axioms less restrictive rather than by deleting them, employing the use of re nement operators. In this paper, we build on previously introduced axiom weakening for ALC, and make it much more irresistible by extending its de nitions to deal with SROIQ, the expressive and decidable description logic underlying OWL 2 DL. We extend the de nitions of re nement operator to deal with SROIQ constructs, in particular with role hierarchies, cardinality constraints and nominals, and illustrate its application. Finally, we discuss the problem of termination of an iterated weakening procedure.
The traditional approach to repairing inconsistent ontologies amounts to
identify problematic axioms and to remove them (e.g., [
2 married :Person
1 married :Person u 1 married :Person Polygamist(mary) (1) (2) (3) (4) According to a classical approach, repairing such an ontology can be done by removing any of the four axioms. However, by removing axiom (1) or (2), we would abandon the polygamist essence of the ontology, by removing axiom (3) we would abandon the more classical view about marriage, and removing axiom (4) trivialises the concept Polygamist. Ideally one wants to preserve as much ? Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). information as possible, and replace these axioms by weaker versions thereof instead of removing them.
Approaches to repair ontologies more gently via axiom weakening were
proposed in the literature [
Re nement operators in Description Logic have been studied with
application to Machine Learning [
In [
In this paper, we extend re nement operators and axiom weakening of [
From a formal point of view, an ontology is a set of formulas in an appropriate
logical language with the purpose of describing a particular domain of interest.
We brie y introduce SROIQ; for full details see [
R; S ::= U j E j r j r
; C ::= ? j > j A j :C j C u C j C t C j 8R:C j 9R:C j
n S:C j n S:C j 9S:Self j fig ; where U and E are the universal role and empty role respectively, r 2 NR, S is simple (see further) in the RBox R, A 2 NC , n is a non-negative integer, and i 2 NI . In the following, L(NC ; NR; NI ) and Lr(NR), denote respectively the set of concepts and roles that can be built over NC , NR, NI in SROIQ. We denote by nnf(C) the negation normal form of the concept C.
The size of a concept in L(NC ; NR; NI ) will be useful in the proofs. We de ne it precisely next.
De nition 1. The size jCj of a concept C is inductively de ned as follows. For C 2 NC [ f>; ?g, jCj = 1. For i 2 NI , jfigj = 1. For R 2 NR, j9R:Self j = 2. Then for R 2 NR and an arbitrary C, j:Cj = 1 + jCj; jC u Dj = jC t Dj = 1 + jCj + jDj; j9R:Cj = j8R:Cj = 1 + jCj, and for a non-negative integer n, j n R:Cj = j n R:Cj = log(n) + 1 + jCj.
A TBox T is a nite set of concept inclusions (GCIs) of the form C v D where
C and D are concepts. It is used to store terminological knowledge regarding
the relationships between concepts. An ABox A is a nite set of formulas of the
form C(a), R(a; b), :R(a; b), a = b, and a 6= b, which express knowledge about
objects in the knowledge domain. An RBox R is a nite set of role inclusions
(RIA) R v S, complex role inclusions R1 R2 v S, and disjoint(R; S) (R and S
simple, see next), where R, R1, R2, and S are roles. A role R 2 NR is simple in
R if it is not implied by any composition of roles; it is non-simple otherwise. An
inverse role R is simple if R is simple. We take U and E as simple. (Transitive,
re exive, irre exive, symmetric, and asymmetric roles can be de ned through
appropriate TBox or RBox axioms.) A SROIQ ontology O = T [ R [ A is
de ned by a TBox T , an RBox R, and an ABox A, where the R is assumed to
be regular, cf. [
The semantics of SROIQ is de ned through interpretations I = ( I ; I ),
where I is a non-empty domain, and I is a function mapping every individual
name to an element of I , each concept name to a subset of the domain, and
each role name to a binary relation on the domain; see [
Given two concepts C and D, we say that C is subsumed by D wrt. the ontology O (C vO D) if CI DI for every model I of O, where we write CI for the extension of the concept C according to I. We write C O D when C vO D and D vO C. C is strictly subsumed by D wrt. O (C @O D) if C vO D and C 6 O D. Given two roles, R and S, R is subsumed by S wrt. the ontology O (R vO S) if RI SI for every model I of O. We may use the shortcuts R O S and R @O S with the obvious interpretation.
De nition 2. Let O be a SROIQ ontology. The set of subconcepts of O is given by sub(O) = f>; ?g [
[ sub(C) [ C(a)2O
[ CvD2O sub(C) [ sub(D) ; where sub(C) is the set of subconcepts in C.
We now de ne the upward and downward cover sets of concept names and atomic roles respectively. Intuitively, the upward cover of the concept C collects the most speci c subconcepts of O that subsume C; conversely, the downward cover of C collects the most general subconcepts from O subsumed by C. The interpretation of the upward and downcover covers of atomic roles is similar. The concepts in sub(O) are some concepts that are relevant in the context of O, and that are used as building blocks for generalisations and specialisations. The properties of sub(O) guarantee that the upward and downward cover sets are nite.
De nition 3. Let O = T [R[A be an ontology. Let C be a concept, the upward cover and downward cover of C wrt. O are:
UpCovO(C) := fD 2 sub(O) j C vO D and DownCovO(C) := fD 2 sub(O) j D vO C and
UpCovO(r) := fs 2 NR [ NR [ fE; U g j r vO s and DownCovO(r) := fs 2 NR [ NR [ fE; U g j s vO r and s; s0 are simple in Rg: s; s0 are simple in Rg: Let n be a non-negative integer:
UpCovO(n) := fn; n + 1g; DownCovO(n) := (fn fng 1; ng when n > 1 when n = 0: In and of themselves, UpCovO and DownCovO miss `interesting' re nements. Example 1. Let NC = fA; B; Cg and O = fA v Bg. Then sub(O) = fA; B; >; ?g. Now UpCovO(A u C) = fAg. Iterating, we get UpCovO(A) = fA; Bg and UpCovO(B) = fB; >g. We could reasonably expect B u C to be also a generalisation of A u C wrt. O but it will be missed by the iterated application of UpCovO, because B u C 62 sub(O). Similarly, UpCovO(9R:A) = f>g, even though we could expect 9R:B to be a generalisation of 9R:A.
To take care of these omissions, we introduce generalisation and specialisation operators that will recursively exploit the structural complexity of the concept being re ned.
Let " and # be two functions with domain L(NC ; NR; NI )[Lr(NR)[N. They map every concept to an element of the powerset of L(NC ; NR; NI ), every role to an element of the powerset of Lr(NR), and every non-negative integers to the powerset of N. We de ne ";#, the abstract re nement operator, by induction on the structure of concept descriptions as shown in Table 1.
We now de ne concrete re nement operators from the abstract operator ";#. De nition 4. The generalisation operator and specialisation operator are dened, respectively, as
O = UpCovO;DownCovO and
O = DowCovO;UpCovO : Returning to Example 1, notice that for NC = fA; B; Cg and O = fA v Bg, we now have O(A u C) = fA u C; B u C; A u >; Ag.
Some comments are in order about Table 1. As in [
De nition 5. Given a DL concept C, its i-th re nement iteration by means of ";# (viz., "i;#(C)) is inductively de ned as follows: { { "0;#(C) = fCg; "j;+#1(C) = "j;#(C) [ SC02 "j;#(C) ";#(C0), j 0.
The set of all concepts reachable from C by means of ";# in a nite number of steps is ";#(C) = Si 0 "i;#(C): 2.1
Basic properties
useful in the remainder of this paper. Lemma 1. For every ontology O:
";#(r ) = fs j s 2 "(r); s 2 NRg [ fs j s 2 "(r); s 2 NR g ";#(U ) = "(U ) ";#(E) = "(E) 1. generalisation: if X 2 O(Y ) then Y vO X
specialisation: if X 2 O(Y ) then X vO Y 2. cover nontriviality: if C 6 O > then there exists some D 2 UpCovO(C) such that C @O D, and if C 6 O ? then there exists some D 2 DownCovO(C) such that D @O C 3. cover triviality: if C O > then > 2 UpCovO(C), and if C O ? then ? 2 DownCovO(C) 4. trivial generalisability: > 2 O(C), U 2 O(r) 5. fgaelnseerhaoloisdastipoencialnisiatebnileistys:: ?O2(C)Oi(sC)n,iEte2 O(r)
specialisation niteness: O(C) is nite Lemma 2. L(NC ; NR; NI ) is closed under O and O. If C 2 L(NC ; NR; NI ) then every re nement in O(C) and O(C) is also in L(NC ; NR; NI ). Proof. (Sketch) The possibly delicate cases involve the re nements of roles. The condition on the upcover and downcover of a role R to contain only simple roles (cf. De nition 3) forces that every re nement of a role is simple. So, the restriction to simple roles guarantees that, e.g., ";#( n R:C) and ";#( n R:C) are in SROIQ, as no complex role may appear in the scope of the cardinality restriction.
Notice that, by dropping that condition, we may have that, e.g., for roles p; q; r; s and axioms r v s, p q v s in O, when generalising from ( n r:C) to ( n s:C) we violate the simplicity condition for roles in cardinality restrictions. tu 2.2
Complexity We now analyse the computational aspects of the re nement operators. De nition 6. Given a SROIQ ontology O and concepts C; D, the problems
O-membership and O-membership ask whether D 2 O(C) and D 2 O(C), respectively.
The re nement operators O and O are e cient, in the sense that
deciding O-membership and O-membership is not harder than deciding concept
subsumption in SROIQ. Recall that subsumption in SROIQ is
N2ExpTimecomplete [
Theorem 1.
O-membership and
O-membership are N2ExpTime-complete.
Proof. (Sketch) We sketch the case of O-membership. The case of O-membership is analogous.
For proving hardness, we rst show that deciding whether C0 2 UpCoverO(C)
is as hard as concept subsumption. Then we show that O-membership is just
as hard. The proofs are identical to the ones in [
For the upper bound, we rst establish the complexity of computing the sets UpCoverO(C), DownCoverO(C), UpCoverO(r), DownCoverO(r). It su ces to check for every D 2 sub(O) whether D 2 UpCovO(C), or D 2 DownCovO(C), and collect those concepts for which the answer is positive. Each check can be done with at most 1 + 4j sub(O)j calls to a SROIQ subsumption sub-routine in non-deterministic double exponential time. The size of sub(O) is linear in the size of T [ A. An analogous exhaustive check of all roles in NR [ fU; Eg permits to compute UpCovO(r), and DownCovO(r). Checking whether a role s is simple in R can be done e ciently.
Finally, we can decide O-membership resorting to at most jCj (one for every subconcept and role in C) computations of the sets UpCovO(r), DownCovO(r),
Overall, the problem of deciding whether D 2 O(C) can be simulated by a deterministic oracle Turing machine with a polynomial number of calls to an N2ExpTime oracle.
Our re nement operators can be used as components of a method for repairing inconsistent SROIQ ontologies by weakening, instead of removing, problematic axioms. In this paper, we do not re ne the RBox, so the regularity of the role hierarchy remains intact in weakened ontologies.
Given an inconsistent ontology O = T [ A [ R, we proceed as described
in Algorithm 1. We rst need to nd a consistent subontology Oref of O to
serve as reference ontology to be able to compute a non-trivial upcover and
downcover. One approach is to pick a random maximally consistent subset of O,
FindMaximallyConsistentSet(O), and choose it as reference ontology Oref; another
is to choose the intersection of all maximally consistent subsets of O (e.g., [
Once a reference ontology Oref has been chosen, and as long as O is inconsistent, we select a \bad axiom" FindBadAxiom(O) (in T [ A) and replace it with a random weakening of it with respect to Oref. We can randomly samples a number of (or all the) minimally inconsistent subsets of axioms I1; I2; : : : Ik O and return one axiom in T [ A from the ones occurring the most often.
The set of all weakenings of an axiom with respect to a reference ontology is de ned as follows: De nition 7 (Axiom weakening). Let O = T [ A [ R be a SROIQ ontology and be an axiom in T [ A. The set of (least) weakenings of is the set gO( ), such that: { gO(C v D) = fC0 v D j C0 2 O(C)g [ fC v D0 j D0 2 O(D)g; { gO(C(a)) = fC0(a) j C0 2 O(C)g; { gO(R(a; b)) = fR0(a; b) j R0 2 O(R)g; { gO(:R(a; b)) = f:R0(a; b) j R0 2 O(R)g; { gO(a = b) = fa = b; ? v >g; { gO(a 6= b) = fa 6= b; ? v >g.
The subprocedure WeakenAxiom( ; Oref) randomly returns one axiom in gOref ( ). For every subsumption or assertional axiom , the axioms in the set gOref ( ) are indeed weaker than , in the sense that { given the reference ontology Oref { entails them (and the opposite is not guaranteed).
Lemma 3. For every subsumption or assertional axiom j=O 0. , if 0 2 gO( ), then Proof. Suppose C0 v D0 2 gO(C v D). Then, by de nition of gO and Lemma 1.1, C0 v C and D v D0 are inferred from O. Thus, by transitivity of subsumption, we obtain that C v D j=O C0 v D0. For the weakening of assertions, the result follows immediately from Lemma 1.1 again. tu
Clearly, substituting an axiom with one axiom from gO( ) cannot diminish the set of interpretations of an ontology: if I is an interpretation that satis es the axioms of ontology before such a replacement, I satis es the same axioms even after it. By Lemma 1.4, any subsumption axiom is a nite number of
Oref FindMaximallyConsistentSet(O) while O is inconsistent do bad FindBadAxiom(O) weaker WeakenAxiom( bad, Oref)
O O n f badg [ f weakerg end while
Return O weakenings away from the trivial axiom ? v >. This holds also for equality and inequality ABox axioms. Any assertional axiom C(a) is also a nite number of generalisations away from the trivial assertion >(a). Similarly, every assertional axioms R(a; b) and :R(a; b) are a nite number of generalisations away from the trivial assertions U (a; b) and :E(a; b), respectively.
Example 2. Consider the ontology O containing the inconsistent set of axioms 1-4 in the introduction. Suppose that FindBadAxiom(O) returns axiom 3 as the most problematic one. According to our de nitions, a possible weakening of the axiom returned by WeakenAxiom(3; Oref) may be MarriedPerson v Person u 2 married :Person u 1 married :Person. Replacing axiom 3 with its weakening, the resulting ontology is consistent.
Example 3. Imagine that the RBox of both our reference ontology Oref and the ontology O contains the following axioms: parent of v ancestor of ; father of v parent of ; mother of v parent of ; parent of parent of v grandparent; disjoint(parent of ; grandparent); parent of child of : And imagine that O includes also the following statements, which cause inconsistency: father of (bob; mary) (1); mother of (mary; alice) (2); child of (alice; bob) (3) A possible resolution of the inconsistency could be the weakening of axiom (3): WeakenAxiom((3); Oref) : ancestor of (alice; bob). 4
As noted by Lemma 1.5 the set of \one-step" re nements of a concept is always
nite. Moreover, Lemma 1.4 indicates that every concept can be re ned in a
nite number of iterations to > (or ?). Nonetheless, an iterated application of
the re nement operator can lead to cases of non-termination. For instance, given
an ontology de ned as O = fA v 9r:Ag, if we generalise the concept A wrt. O
it is easy to see that we can obtain an in nite chain of generalisations that never
reaches >, i.e., A vO 9r:A vO 9r:9r:A : : : For practical reasons this may need
to be avoided, or mitigated. Running into this non-termination `problem' is not
new in the DL literature. In [
Another possibility is to abandon certain termination and adopt almost-sure termination, that is, termination with probability 1. The idea is to associate probabilities to the re nement `branches' available at each re nement step.
In what follows we will show that, indeed, if we start from any concept C and choose uniformly at random a generalisation out of its set of possible generalisations (or a re nement out of its set of re nements: the proofs are entirely symmetrical) we will almost surely reach > (?) within a nite number of steps. This implies at once that an axiom will almost surely not be inde nitely weakened by our procedure, and that Algorithm 1 will almost surely terminate.
The key ingredient of the proof is Lemma 4, which establishes an upperbound on the rate of growth of the set of possible generalisations (re nements) along a chain.
De nition 8. Let O be a SROIQ ontology and let C 2 sub(O). Then let F (C) = j O(C)j be the number of generalisations of C, let F 0(C) = j O(C)j be the number of specialisations of C and let G(C) = max(fjC0j j C0 2 O(C) [
O(C)g) be the maximum size of any generalisation or specialisation of C. By setting an upper bound to the size of (C) and (C), part 1 of the following lemma may in particular be seen as a quantitative version of Lemma 1.5. Lemma 4. Let O be a SROIQ ontology and let C be any concept (not necessarily in sub(O)). Furthermore, let k = j sub(O)j + 2jNRj + 2 and q = max(fjCj; jnnf(:C)j j C 2 sub(Og). Then 1. F (C); F 0(C) 3kjCj; 2. G(C) jCj + q.
Proof. The full proof via structural induction is lengthy but presents no particular di culties. The intuition behind it is the following: by our de nitions, in a generalisation/specialisation step we essentially select a single subcomponent C0 (or r) of the current expression C and we replace it with some element of sub(O) (or of NR [NR ). But these two sets are nite, and the number of subcomponents of an expression C increases linearly with the size of C. Thus, the number of possible generalisations/specialisations of C increases linearly with the size of C, and every generalisation/specialisation step increases the size of the resulting expression by some at most constant amount. tu We can now prove our required result by showing that, even though the size of the concept expression { and, therefore, the number of possible generalizations { grows with every generalization step, it grows slowly enough that the generalization chain will almost surely eventually pick an element in the upcover of the current concept which is strictly more general than it. Thus, > will be almost surely reached in a nite number of steps.
Theorem 2. Let O be a SROIQ ontology, let C be any SROIQ concept, and let (Ci)i2N be a sequence of concepts such that C0 = C and each Ci+1 is chosen randomly in O(Ci) according to the uniform distribution.
Then, with probability 1, there exists some i 2 N such that Ci = >. Proof. Let us rst prove that, if C 6 O >, there is almost surely some Ci in the chain such that Ci O > (and, therefore, such that Ci0 O > for all i0 > i).
By the previous lemma, we know that O(Ci) contains at most 3kjCij concepts. Furthermore, for every concept Ci such that Ci 6 O > there exists at least one C0 2 UpCovO(Ci) O(Ci) such that C @O C0 (c.f., Lemma 1.2): therefore, the probability that the successor of Ci will be some Ci+1 2 UpCovO(Ci) such that Ci @O Ci+1 is at least 1=(3kjCij). Now let jC0j = N : since Ci+1 2 O(Ci), we then have that jCij qi + N . Therefore, the probability that at step i we do not select randomly an element of UpCovO(Ci) that is strictly more general than Ci will be at most 3k3(kq(iq+i+NN) ) 1 = i+i +`` for ` = N=q and = 1=(3kq). But then the probability that we never select a strictly more general element from the upcover will be at most Qi1=0 i+i +`` = 0,3 and thus our generalisation sequence C = C0 vO C1 vO C2 : : : will almost surely contain some Ci such that Ci+1 2 UpCovO(Ci) sub(O) and C vO Ci @O Ci+1. By the same argument, the generalisation sequence starting from Ci+1 will almost surely eventually reach some Cj+1 2 sub(O) with C @O Ci+1 @O Cj+1, and so forth; and by applying this line of reasoning j sub(O)j times, we will almost surely eventually reach some concept D O >, as required.
Now let us consider a generalisation chain D = D0 vO D1 vO D2 : : :, where as before every Di+1 is chosen randomly among (D), starting from some concept D O >. Now, since D O > and D vO Di for all i, > 2 UpCovO(Di) O(Di) for all i (c.f., Lemma 1.3). Thus, at every iteration step i we have a probability of at least 1=j (Di)j that Di+1 = >; and if we let N 0 = jDj, by the previous results we obtain at once that j (Di)j iq + N 0, and hence that the probability that we do not end up generalising Di to > is at most (3k(iq + N 0) 1)=(3k(iq + N 0)), and nally that the probability that we never reach > is Qi1=0 3k3(ki(qi+q+NN0)0) 1 = Q1 i+`0 0 = 0 where `0 = N 0=q and 0 = 1=3kq.
i=0 i+`0 tu
Note that, by our de nitions, > can be further generalized to all elements of its upcover (that is, all concepts of sub(O) which are equivalent to > with respect to O), and similarly ? can be further specialized to other concepts in its downcover. If this behaviour is unwanted, it is easy to force the upcover of > to contain only >, and likewise for ?; but regardless of this, our results imply 3 One way to verify this is to observe that the series Pi1=0(log(i + ` ) log(i + `)) diverges to minus in nity. This in turn may be veri ed by noting that Pi1=0(log(i + ` ) log(i + `)) Pi1=0(log(i + d`e ) log(i + d`e)) = Pi1=d`e(log(i ) log(i)), because log(i + ` ) log(i + `) log(i + d`e ) log(i + d`e), and then showing that Pi1=d`e(log(i ) log(i)) = Pi1=d`e log(i) log(i ) diverges to plus in nity by means of the integral method: the terms of the series are all positive, and RdU`e log(x) log(x )dx goes to in nity when U goes to in nity. Since the integral diverges, so does the series, which gives us our conclusion. at once that every axiom will almost surely be weakened into > v ? in a nite number of weakening steps. 5
We presented a set of re nement operators covering most aspects of the full
SROIQ language. Further additions to the general rules of re nements may
be studied, e.g. those governing re nements of roles that can be obtained by
considering complex roles in the up and down covers. Re nement operators have
so far been implemented for the ALC fragment. This implementation will need
to be extended to deal with the SROIQ re nement operators presented here.
As done in [