that forms a T -violation set for t in clT (A ∪ {α}**). Now suppose that, for every** t ∈ T \ T +, and for every T -violation set V in clT (A ∪ {α}), V **does not contain** α. This means that either (i) there is no T -violation set in clT (A ∪ {α}**), or** (ii) all T -violation sets in clT (A ∪ {α}) do not contain α**. Btoh cases lead to a**
contradiction, and, therefore, we conclude that there is a T **-violation set** V in clT (A ∪ {α}) such that V contains α. Finally, since hT , {α}i **is satisfiable, it is** immediate to verify that (V \ {α}) ⊆ clT (A).

The next theorem is the key to our solution.

Theorem 7. Let α be an atom such that α ∈ clT (A) \ clT (F). There exists a maximal subset Σ of clT (A) such that hT , Σ ∪ Fi is satisfiable and Σ does not contain α if and only if there is a T -violation set V in clT (A)∪clT (F) such that α ∈ V , and hT , F ∪ (V \ {α})i is satisfiable.

Proof (sketch). (⇒) Suppose that there is a T **-violation set** V in clT (A)∪clT (F)
such that α ∈ V and hT , F ∪ (V \ {α})i is satisfiable. Since hT , F ∪(V \ {α})i is satisfiable, the set of maximal subsets Σ of clT (A) such that hT , Σ∪F∪(V \{α})i is satisfiable is non-empty. Consider any Σ **in such a set, i.e., assume that** Σ is a maximal subset of clT (A) such that hT , Σ ∪ F ∪ (V \ {α})i **is satisfiable. It**
can be shown that (1) Σ does not contain α, and (2) Σ **is a maximal subset of**
clT (A) such that hT , Σ ∪ Fi **is satisfiable.**
(⇐) Suppose that there is no T -violation set V in clT (A)∪clT (F**) such that**
α ∈ V and hT , F ∪ (V \ {α})i **is satisfiable. We show that every maximal subset**
Σ′ of clT (A) such that hT , Σ′ ∪ Fi is satisfiable contains α**, by showing that, if**
Σ is a subset of clT (A) such that hT , Σ ∪Fi is satisfiable, then hT , Σ ∪F ∪ {α}i is also satisfiable. Indeed, assume by way of contradiction that hT , Σ ∪F ∪ {α}i is unsatisfiable. Note that α ∈ clT (A), and, since hT , Ai **is satisfiable,** hT , {α}i is also satisfiable. We can therefore apply theorem 6, and conclude that there is a T -violation set V in clT (F ∪ Σ ∪ {α}) such that (1) V contains α**, (2)**
(V \ {α}) ⊆ clT (F ∪ Σ). Now, since (V \ {α}) ⊆ clT (F ∪ Σ), and hT , Σ ∪ Fi is satisfiable, it follows that hT , F ∪ (V \ {α})i **is satisfiable. This implies that**
there is a T -violation set V in clT (F ∪ Σ ∪ {α}) ⊆ clT (A) ∪ clT (F**) such that**
α ∈ V and hT , F ∪ (V \ {α})i **is satisfiable, which is a contradiction.**
Theorems 6 and 7 allow us to prove that K ⊕T∩ F **can be computed by the**
algorithm ComputeInsertion **below.**
Algorithm ComputeInsertion requires to compute all T **-violation sets in**
clT (A)∪clT (F**). It can be shown that this can be done by computing the results** of suitable conjunctive queries posed to clT (A) ∪ clT (F**). Such queries are built**
out of the negative inclusion assertions and the identification assertions Tid in T **, and essentially look for tuples that satisfy the negation of such assertions.** From this observation, one can derive the following theorem.

Theorem 8. **ComputeInsertion**(hT , Ai, F) terminates, and computes hT , Ai⊕T∩
F in polynomial time with respect to |T \ Tid|, |A|, and |F|, and in NP with respect to |Tid|.