It is immediate to verify that, up to logical equivalence, the result of **changing**
hT , Ai with the insertion or the deletion of F **is unique. In the rest of this** paper, the result of changing K = hT , Ai **with the insertion (resp. deletion) of** F
according to our semantics will be denoted by K ⊕T∩ F (resp. K ⊖T∩ F**). Notice**
that, by definition of our operator, in the case where F **is inconsistent with** T , the result of changing hT , Ai **with both the insertion and the deletion of** F is logically equivalent to hT , Ai **itself.**
Example 2. **Consider the** DL-LiteA,id KB K **of the Example 1, and suppose**
that p becomes now a race director, and b **becomes the new official driver ofq** team t1. To reflect this new information, we change K **with the insertion of** F1 = {RD(p), OD(b), mf(b, t1)}**. Since the TBox implies that a race director**
cannot be a team member, RD(p) contradicts TM(p**). Also, since every team has** at most one official driver, OD(b) and mf(b, t1) contradict mf(s, t**). According** to Definition 3, the KBs accomplishing the insertion of F1 into K **minimally are:**
K1 = hT , {RD(p),OD(b),mf(b, t1),TM(s),mf(**s, t**1)}i K2 = hT , {RD(p),OD(b),mf(**b, t**1),TM(s),OD(s)}i Thus, K ⊕T∩ F1 is:

## K3 = Ht , {Rd(P),Od(B),Mf(**B, T**1),Tm(S)}I.

Now, suppose that we do not know anymore whether b is a member of t1**, and,** even more, whether b is a team member at all. Then, we change K3 **with the**
deletion of F2 = {TM(b), mf(b, t1)}**, thus obtaining**

## K3 ⊕T∩ F2 = Ht , {Rd(P),Tm(S),Od(B)}I.

Comparison with related work. **We mentioned in the introduction several**
model-based approaches to DL KB evolution, and noticed that they **all suffer** from the expressibility problem. This problem is also shared by [15], that uses features **instead of models, and proposes the notion of approximation to cope** with the expressibility problem, similarly to [7].

Related to our proposal are several formula-based approaches **proposed in**
the literature. We already pointed out that our proposal is inspired **by [8], although the problem studied in [8] is evolution in propositional logic, whereas**
the context dealt with in our work is instance-level evolution in DLs. Perhaps, the closest approach to the one proposed in this paper is that reported in [6],
where formula-based evolution (actually, insertion) of DL-Lite **KBs is studied.** The main difference with our work is that we base our semantics on the **WIDTIO** principles, and therefore we compute the intersection of all KBs accomplishing the change minimally. Conversely, in the bold **semantics discussed in [6], the result of the change is chosen non-deterministically among the KBs accomplishing**
the change minimally. Another difference is that while [6] addresses the issue of evolution of both the TBox and the ABox, we only deal with the case of fixed TBox (in the terminology of [6], this corresponds to keep the TBox protected).

It is interesting to observe that the specific DL considered in [6] is DL-LiteFR,