Knowledge engineers might face situations in which an unwanted consequence is derivable from an ontology. It is then desired to revise the ontology such that it no longer entails the consequence. For this purpose, we introduce a novel technique for repairing TBoxes formulated in the description logic EL. Speci cally, we rst compute a canonical model of the TBox and then transform it into a countermodel to the unwanted consequence. As formalism for the model transformation we employ transductions. We then obtain a TBox repair as the axiomatization of the logical intersection of the original TBox and the theory of the countermodel. In fact, we construct a set of countermodels, each of which induces a TBox repair. For the actual computation of the repairs we use results from Formal Concept Analysis.
Description logics (DLs) are a family of logic-based knowledge representation
languages, supporting terminological knowledge (a schema) as well as assertional
knowledge (the data). Common reasoning services allow for deducing implicit
consequences that logically follow from the explicitly stated knowledge.
Sometimes, we encounter situations where the derivation of such a consequence must
be made impossible | either because it is invalid in the underlying domain of
interest, or since it is privacy-sensitive information that needs to be hidden.
The classical approach to repairing a knowledge base in such situations is to
remove axioms such that the remaining axioms do not entail the unwanted
consequence anymore, i.e., a classical repair is a subset of the given knowledge base.
As a downside, also other consequences might vanish that are actually wanted.
Speci cally, the computation of classical repairs is based on justi cations, which
are minimal subsets of the ontology that entail the unwanted consequence | as
pointed out in [
More ne-grained repairs | in the sense that not too many other
consequences are a ected | can be obtained if axioms are weakened instead of
removed completely [
However, weakening axioms is not the only way to obtain such a non-classical
repair. In this document, we speci cally consider the problem of repairing a TBox
with respect to a given concept inclusion (the unwanted consequence), all within
the light-weight description logic EL for which most common reasoning tasks
can be solved in polynomial time [
To describe the construction of suitable countermodels, we utilize the
formalism of transductions [
The structure of this document is as follows. In the next Section 2 we brie y recall important notions of the description logic EL. Section 3 describes transductions that can be utilized to construct countermodels, and Section 4 explains how the logical intersection (of a TBox and a countermodel) can be axiomatized. We close this document with some concluding remarks in Section 5.
We presume familiarity with basic notions of the description logic EL. Given a signature := C [ R consisting of concept names and role names, EL concept descriptions are built from using the constructors >, u, and 9. Throughout this document we assume that all signatures are nite. (Nested) conjunctions are treated like sets, i.e., nestings, repetitions, and order are irrelevant. An atom is either a concept name or an existential restriction. Every concept description C is a conjunction of atoms, the top-level conjunction of C, and the set of all these atoms is denoted as Conj(C). Speci cally, > is the empty conjunction. Given a concept C, we denote by Sub(C) the set of all subconcepts of C (including C itself) and Atoms(C) is the subset containing all atoms occurring as subconcepts in C. Likewise, Sub(T ) consists of all subconcepts occurring in T . We say that an interpretation I satis es a concept inclusion (CI) C v D, written I j= C v D, if CI DI . Given a concept inclusion C v D and a TBox T , we say that T entails C v D and that C is subsumed by D w.r.t. T , written T j= C v D and C vT D, respectively, if each model of T satis es C v D. 3
Constructing Countermodels by Model Transformation Within this section, we are going to develop a method that produces countermodels to a concept inclusion entailed by a TBox. For this purpose, assume that T is a TBox and further that C v D is a concept inclusion, both formulated in the description logic EL, such that T entails C v D. We start with formally de ning the notion of a countermodel.
De nition 1. Let C v D be a concept inclusion. A countermodel to C v D is an interpretation that does not satisfy C v D.
Note that an interpretation I is a countermodel to C v D if and only if I contains a domain element d such that d 2 CI and d 62 DI . Of course, such a countermodel can only exist if C v D is no tautology, i.e., if it is not valid in all interpretations | we thus assume further that C v D satis es this condition. 3.1
The Underlying Idea of the Countermodel Construction As a starting point for constructing suitable countermodels we use the canonical model IC;T induced by the premise C and the TBox T , because it contains an element dC that is already an instance of C and, since it is a model of T , this element dC is also an instance of D. In order to obtain a countermodel we will modify IC;T in a way such that the distinguished element dC is still an instance of C but not an instance of D anymore.
De nition 2. [
IC;T := fdC g [ fdC0 j 9r:C0 2 Sub(C) [ Sub(T )g
AIC;T := f dD j T j= D v A g
rIC;T := f (dD; dD0 ) j T j= D v 9 r: D0 and 9 r: D0 2 Sub(T ) [ Conj(D) g
To appropriately modify the canonical model, we adopt a technique for
repairing DL ABoxes that was introduced in [
To minimize the amount of information lost by such a repairing process, this technique does not only remove assertions from A, but also splits objects by introducing copies of them, which are created based on sets of atoms occurring in P . In particular, for each object u from the input ABox, exponentially many copies yu;K are introduced, where each K is a subset of Atoms(P ). These copies are then used as objects in the ABox repair, and the assertions in the repair are computed in a way such that each yu;K is not an instance of every atom in K.
In order to adapt the aforementioned repair technique to an approach to constructing countermodels, we view the canonical model IC;T as the ABox A, the right-hand side D of the concept inclusion C v D as the concept P , and the distinguished element dC as the individual name a. In particular, each domain element of the countermodel will be a copy of a domain element of IC;T indexed by a set K Atoms(D), and the interpretation function is de ned in a way such that each copy is not in the extension of each atom in K. We use the formalism of transductions for precisely describing the transformation of the canonical model.
As preparation, we rst de ne a transduction in its most basic setting.
De nition 3. [
We now introduce a functional transduction repair;D that resembles the
transformation of an ABox into compliant anonymizations as in De nition 11 of [
I ; K Atoms(D); d 2 F I for each F 2 K; and K does not contain v;-comparable atomsg A repair;D(I) := fdK j d 2 AI and A 62 Kg r repair;D(I) := f(dK; eL) j (d; e) 2 rI and for each 9r:Q 2 K with e 2 QI ; there is F 2 L such that Q v; F g In particular, repair;D is a copying transduction with index set P(Atoms(D)). Example 5. Consider the TBox T = fA v A1; B v B1 u B2g and the concept inclusion C v D := A u 9r:B v A1 u 9r:(B1 u B2), which is entailed by T but is no tautology. The canonical model IC;T of C w.r.t. T is illustrated in Figure 1.
A; A1 dC r
B; B1; B2
dB
Applying the transduction repair;D to the canonical model IC;T yields a countermodel to C v D that is depicted in Figure 2. The gray nodes represent the elements that are an instance of C but not an instance of D.
A; A1 dC;; r
A dC;fA1g
A; A1 dC;f9r:(B1uB2)g
A dC;fA1;9r:(B1uB2)g dB;; B; B1; B2 dB;fB1g B; B2 dB;fB2g B; B1 dB;fB1;B2g
B
Proposition 6. For each EL TBox T and each non-tautological concept
inclusion C v D entailed by T , the interpretation repair;D(IC;T ) is a countermodel
to C v D.
Proof. It is a nger exercise to adapt Lemmas 13 and 18 in [
Obtaining Countermodels Using MSO Transductions
As seen above, transductions can be de ned using a mathematical
metalanguage | it is only necessary to describe all interpretations in the image,
including their domains and their interpretation functions. A more formal
approach to describing transductions is by using well-formed logical formulae. In
the following, we introduce monadic second-order (MSO) transductions as
formalism to describe model transformations, which is generally de ned in [
An MSO transduction maps an input interpretation to output interpretations according to a tuple of MSO formulae called de nition scheme. A de nition scheme consists of formulae that de ne the domain, and the concept and role extensions. The domain formula of a de nition scheme contains one free variable | and every element of the input interpretation that satis es this formula is then an element of the output interpretation. The concept and role extensions of the output interpretation are de ned accordingly by concept formulae and role formulae | there is one concept formula for each concept symbol and role formula for each role symbol of the signature. For copying transductions, a de nition scheme contains families of these formulae for the elements of the respective ( nite) index set.
By MSO( ; W), we denote the set of MSO formulae built over a signature
and a nite set W of rst-order and set variables, which are free in the respective
formula. For a detailed introduction to rst-order logic (FOL) and MSO, we refer
the reader to [
De nition 7. [
D = ( ; ( i)i2I; ( A;i)(A;i)2 C I; ( r;i;j )(r;i;j)2 R I I) consisting of { a precondition formula
2 MSO( ; W), 1 We write dC;K instead of (dC )K. 2 In general, MSO transductions allow for monadic second-order variables (often called set variables). However, we will only make use of rst-order variables as parameters. { domain formulae i 2 MSO( ; W [ fxg) for each i 2 I, { concept formulae A;i 2 MSO( ; W [ fxg) for each (A; i) 2 { role formulae r;i;j 2 MSO( ; W [ fx; yg) for each (r; i; j) 2 C R
I, and I I.
De nition 8. [
I ; i 2 I; and (I; ) j= i(d)g AD^(I; ) := fdi j (I; ) j=
A;i(d)g rD^(I; ) := f(di; ej ) j (I; ) j= r;i;j (d; e)g (I; ) j= i(d) means (I; 0) j= i(x) where 0 extends by 0(x) := d (and accordingly for and ).3 The transduction D induced by D is de ned as D := f(I; D^ (I; )) j is a W-assignment in I with (I; ) j= g:
As already mentioned, we consider MSO transductions as means of model
transformation to ensure that our model transformations are well de ned, and to
only use logical notions. Another important bene t is that MSO transductions
are always computable since MSO model checking is decidable | in fact, it is
PSpace-complete [
In order to de ne an MSO transduction that is equivalent to repair;D, we need to devise a de nition scheme Drepair;D such that its induced transduction Drepair;D equals repair;D. We have already seen above that the index set I = P(Atoms(D)) is used. Further recall that repair;D needs to check the condition \for each 9r:Q 2 K with e 2 QI , there is F 2 L such that Q v; F " during the creation of the interpretation function. In particular, it must be determined whether a concept inclusion is a tautology, i.e., is satis ed in all interpretations. One might be tempted to translate this condition into a conjunct of the formulae r;K;L as follows, where we denote by C# the FOL-translation of a concept C. r;K;L(x; y) := r(x; y) ^
Q#(y) !
_ 8z : Q#(z) ! F #(z) ^ 9r:Q2K However, during the computation of the image of an interpretation I it will only be checked whether this conjunct is satis ed in I (and not in all interpretations).
There are two ways to resolve this issue. Firstly, instead of de ning the formula r;K;L directly, we could provide a construction speci cation in which we externalize the problematic condition, e.g., as follows.
r;K;L(x; y) := 8>r(x; y) if, for each 9r:Q 2 K with y 2 QI ; < there is an atom F 2 L s.t. Q v; F > :?
otherwise 3 We will later write (W; x) instead of (z1; : : : ; zn; x) for W = fz1; : : : ; zng. Secondly, we could generalize the formalism of MSO transductions in that the formulae of the de nition scheme are not evaluated in the input interpretation I but instead it is checked whether they are tautologies. If some subformulae must be evaluated in I, we could simply precede them with \ I# ! " where I# is the FOL-translation of I, i.e., I# := Vd2AI A(d) ^ V(d;e)2rI r(d; e). With that modi cation, we are then able to specify the role formulae as r;K;L(x; y) := (I# ! r(x; y)) ^ (I#
! Q#(y)) ^ 9r:Q2K ! _ (8z : Q#(z) ! F #(z)) :
Going with the second solution, however, leads to the e ect that MSO transductions are not necessarily computable anymore because MSO is generally not decidable. If we were to restrict the conditions to decidable logics, then computability of transductions is ensured, but becomes less expressive.
Having the interpretation repair;D(IC;T ) computed, there are possibly multiple nodes that satisfy concept C and not concept D. Each of these nodes together with their reachable elements are countermodels to the unwanted consequence of the TBox. We de ne a transduction that cuts out reachable parts for every node that is in C and not in D. The result is a set of countermodels.
We are making use of an auxiliary predicate for reachability of two elements
in an interpretation I, denoted by reach(x; y). An edge between two elements,
expressed by succ(x; y), is de ned as Wr2 R r(x; y) for a given signature .
reach(x; y) := 8X : x 2 X ^ (8x; y : x 2 X ^ succ(x; y) ! y 2 X) ! y 2 X
The formula reach(x; y) is true for two elements in a given interpretation
I if and only if they belong to the re exive and transitive closure of the succ
relation in the interpretation I [
The transduction reach de ned below is used to extract a set of countermodels from interpretations repair;D(I). For this purpose, we use rst-order parameter variables and no index set (non-copying). Recall that, for every variable assignment such that (I; ) j= , a transduction yields another output interpretation. Thus, we obtain a set of countermodels for each -satisfying assignment . De nition 9. Let be a signature and let v be a rst-order parameter in W. The de nition scheme Dreach inducing the transduction reach consists of the formulae:
(W) := C#(v) ^ :D#(v) (W; x) := reach(v; x)
A(W; x) := A(x) for each A 2 r(W; x; y) := r(x; y) for each r 2
C R: Theorem 10. Let T be an EL TBox, let C v D be an unwanted consequence of T , and assume that C v D is no tautology. Then, reach( repair;D(IC;T )) is a set of countermodels to C v D. Example 11. Coming back to Example 5, the application of rst repair;D and then reach to the canonical model IC;T yields a set consisting of three countermodels to A u 9r:B v A1 u 9r:(B1 u B2) with roots dC;fA1g; dC;f9r:(B1uB2)g, and dC;fA1;9r:(B1uB2)g, respectively. For instance, in addition to the root element dC;fA1g, the rst countermodel consists of the r-successors dB;;, dB;fB1g, dB;fB2g, and dB;fB1;B2g, each of which is coloured with green in Figure 2.
While the canonical model IC;T of a concept C w.r.t. a TBox T is
computable in polynomial time [
Constructing Repairs by Axiomatizing the Logical
Intersection
The goal of this section is to explain how a countermodel can be used for
computing a repair. Speci cally, we only consider the case of repairing an EL TBox T
for an unwanted EL concept inclusion C v D. It is irrelevant for our purposes
for what reason the concept inclusion is unwanted | for instance, it might be
an erroneous consequence, or it might be sensitive information that needs to be
hidden. We start with the formal de nition of a repair, which is De nition 1
in [
De nition 13. Consider a TBox T that entails a concept inclusion C v D. A repair of T for C v D is a TBox that is entailed by T and that does not entail C v D.
In contrast to classical repairs, we not only consider subsets of T as repair candidates, but arbitrary TBoxes entailed by T . This leaves much more room for ne-grained repairs.
Now assume that J is a countermodel to the unwanted consequence C v D,
e.g., one that is constructed from the canonical model IC;T according to
Theorem 10 or, alternatively, one that has been built by an expert in the domain that
underlies T . In order to construct a repair, the idea is to axiomatize the logical
intersection of the TBox T and the countermodel J . This logical intersection
T J consists of all concept inclusions that are both entailed by T and
satised by J . It immediately follows that T entails T J and further that T J
does not entail C v D. The only reason that prevents us from directly using
T J as a repair is, in general, its in nite size. To overcome this obstacle, we
need to axiomatize it with only nitely many concept inclusions. We solve the
axiomatization task by means of the results in Section 6 in [
First of all, we introduce a common abstraction of the two notions of TBoxes and interpretations, namely both induce so-called closure operators. Such a closure operator (clop) maps each concept description E to a concept description E such that E v; E (extensive), E v; F implies E v; F (monotone), and (E ) ; E (idempotent ). We say that a concept inclusion E v F is valid for if the closure E is subsumed by F , i.e., E v; F .
As described in Section 4.3 in [
Example 14. Consider the concept C = A u 9 r: B and the TBox T = fA v A1; B v B1 u B2g from Example 5. The most speci c consequence of C w.r.t. T is the concept C T = A u A1 u 9 r: (B u B1 u B2). It is subsumed by the concept D = A1 u 9 r: (B1 u B2) in Example 5, i.e., the concept inclusion C v D is valid for the induced closure operator T .
Furthermore, as shown in [
Example 15. Consider the interpretation J the domain of which consists of the four elements in Figure 2 with a double outline. We are going to compute the closure of the concept C from Example 5. Firstly, we determine the extension CJ , which consists only of dC;f9r:(B1uB2)g. Secondly, we construct the model-based most speci c concept of CJ , which yields the closure C J = A u A1 u 9 r: (B u B2) u 9 r: (B u B1) u 9 r: B. This concept is not subsumed by the concept D from Example 5, i.e., the CI C v D is not valid for the induced closure operator J .
The set of all closure operators is a lattice [
As shown in [
Finally, we utilize the technique in Section 6.6 in [
Another reason why a role-depth bound needs to be employed is to guarantee
niteness of the canonical base. As shown in Section 6.3 in [
In summary, we obtain the following result.
Theorem 17. For each countermodel J to C v D and for each role-depth bound n 2 N, the canonical base Can(( T J ) n) is a repair of T for C v D.
The actual computation of the above canonical base utilizes methods from
Formal Concept Analysis (FCA). We will not go into detail here and rather refer
interested readers to Section 6 in [
Example 18. Reconsider the TBox T as well as the concept inclusion C v D from Example 5 and one of the countermodels from Example 11, namely the one with root dC;f9r:(B1uB2)g, which consists of the domain elements depicted in Figure 2 by the four nodes with a double outline. Denote this countermodel by J . Of the canonical base of T J restricted to role depth 1, we computed the part consisting of all CIs where each conjunction has at most three conjuncts: { A v A1, { B u E v B1 u B2 where E is a concept name di erent from B; B1; B2, or
E is an existential restriction 9 s: > for a role name s, { 9 r: B v 9 r: (B u B1) u 9 r: (B u B2), { 9 s: B v 9 s: (B u B1 u B2) where s is a role name di erent from r, { 9 r: (B u B1) u 9 r: (B u B2) u E v 9 r: (B u B1 u B2) where E is a concept name di erent from A; A1; B, or E is an existential restriction 9 r: F for a concept name F di erent from A; B; B1; B2, or E is the existential restriction 9 r: (B1 u B2), or E is an existential restriction 9 s: > for a role name s 6= r We observe that one of the r-successors of the root dC;f9r:(B1uB2)g would su ce to constitute a countermodel to C v D. Speci cally, for the countermodel consisting only of the root and the single r-successor dB;fB1g, the CI B v B2 is contained in T J and thus entailed by the repair.
The above example shows that a repair in form of a canonical base
(CBrepair) might get considerably larger than the input TBox. Alternatively, a
countermodel J could be used to only weaken the axioms in the TBox T in
order to get a repair: for each CI E v F in T , replace its right side F with
the least common subsumer of F and E J . The resulting TBox is entailed by
T and has J as a model, which implies that it does not entail the unwanted
consequence C v D. It follows that each such repair quali es as a gentle
repair in the sense of [
This article discusses an approach to repairing EL TBoxes such that they do not entail unwanted consequences in the form of CIs. In particular, this approach is realized by rst transforming the canonical model of the left-hand side of the CI w.r.t. the given TBox into a countermodel to the CI. We adapt a technique for computing ABox repairs and we use transductions as formalism for the model transformation. Instead of only constructing one countermodel, our approach is also equipped with a technique that yields a set of countermodels to the CI. A TBox repair is nally obtained as the axiomatization of the logical intersection of the original TBox and a constructed countermodel.
As seen in Example 18, we could further re ne the second transduction reach
such that not all reachable elements are included, but only enough to obtain a
countermodel. To complete our complexity results, a further study on the
complexity of computing a TBox repair from a given countermodel will be necessary
as a next step. In [