

![0_image_0.png](0_image_0.png)

## 5 Insertion In Dl-Lite**A,Id**

We refer to a DL-LiteA,id-KB K = hT , Ai, and we address the problem of changing K with the insertion of a finite set F **of ABox assertions. As in the previous**
section, we assume that both hT , Ai and hT , Fi **are satisfiable. The main problem to be faced with insertion is described by the following observation.**
Suppose that T contains n **identification assertions with at least two atoms**
that become simoultaneously violated with the insertion of a single ABox assertion f into hT , Ai**, and such that every choice of retracting one of such atoms**
yields a maximal subset of clT (A) that is T -consistent with f**. Obviously, there**
are at least 2n **such maximal subsets. What the above example shows is that,**
given f**, there can be an exponential number of maximal subsets** A′ of clT (A)
such that hT , A′ ∪ {f}i **is satisfiable. Note that this cannot happen in those**
DLs of the DL-Lite **family which do not admit the use of identification assertions (such as the DL studied in [6]). Indeed, in such logic, there is always one**
maximal subset of clT (A) that is consistent with a set F **of ABox assertions.**
It follows from the above observation that building all maximal subsets of hT , Ai which are T -consistent with F**, and then computing their intersection**
is computationally costly. Fortunately, we show in the following that we can compute K ⊕T∩ F **without computing all maximal consistent subsets of** hT , Ai with F.

To describe our method, we need some preliminary notions. A set V **of facts**
is called a T -violation set for t ∈ T \ T + if hT + ∪ {t}, V i **is unsatisfiable, while**
for every proper subset V
′ of V , hT + ∪ {t}, V ′i is satisfiable. Any set V **of facts**
that is a T -violation set for a t ∈ T \ T + **is simply called a** T -violation set.

Theorem 6. Let hT , Ai be a satisfiable DL-Lite**A,id**-KB, and let α be an ABox assertion such that hT , {α}i is satisfiable. If hT , **A ∪ {**α}i is unsatisfiable, then there is a T -violation set V in clT (**A ∪ {**α}) such that (i) V contains α, and (ii) (V \ {α}) ⊆ clT (A).

Proof (sketch). We first show that, if hT , A ∪ {α}i **is unsatisfiable, then there**
is a TBox assertion t in T \ T + such that hT +, A ∪ {α**}i |**= q t**, where** q tis the boolean query corresponding to the negation of t**. This implies that there**
is a query q
′in the T **-expansion of** q tthat evaluates true on clT (A ∪ {α}), i.e.,