Splitting and Updating Hybrid Knowledge Bases (Extended Version) 53 because I
′coincides with J on P \ U. There must also exist some predicate symbol P0 such that diff (P0, I′, J′′) ( diff (P0, I′, J) .

Since this is impossible if P0 belongs to P \ U, P0 must belong to U. Now let J
′′′ =
J
′′[U] ∪ J
′[P\U]. For predicate symbols P ∈ U we have diff (P, I, J′′′) = diff (P, I′, J′′) ⊆ diff (P, I′, J) = diff (**P, I, J**′)
and for predicate symbols P ∈ P \ U we have diff (P, I, J′′′) = diff (**P, I, J**′) = ∅ .

Also, for P0 we obtain diff (P0, I, J′′′) = diff (P0, I′, J′′) ( diff (P0, I′, J) = diff (P0**, I, J**′)
As a consequence, J
′′′ <I J
′, which is in conflict with the assumption that J
′ belongs to I ⊕ N.

Proposition 101 Let U be a set of predicate symbols and U = hUiii<n be a finite sequence of first-order theories such that for every **i < n**, pr(Ui) is included in U. Then the minimal change update model of U is saturated relative to U.

Proof Follows using induction on i by Proposition 29 and by Lemma 100.

Proposition 102 Let U = hUiii<n be a finite sequence of first-order theories, U be a splitting sequence for U and S = hSαiα<µ be the saturation sequence induced by U. If M is the minimal change update model of U, then M is sequence-saturated relative to S and for every ordinal **α < µ**,
σ(**M, S**α) is the minimal change update model of bSα(U).

## Proof

We prove by induction on n.

1
◦If n = 0, then U = h i, so M = I by definition. Thus, M is trivially sequencesaturated relative to S. Moreover, for every **α < µ**, bSα(U) = h i, and σ(**M, S**α) =
σ(I, Sα) = I, so σ(**M, S**α) is the minimal change update model of bSα(U).

2
◦ We assume the claim holds for n and prove it for n + 1. Suppose M′is the minimal change update model of U
′ = hUiii<n+1. It follows from Proposition 90 that M′ =
M ⊕ N where M is the minimal change update model of U = hUiii<n and N is the MKNF model of Un. We need to prove that for every α < µ, σ(M′, Sα) is the minimal change update model of bSα(U
′).

Take some arbitrary but fixed **α < µ**. By the inductive assumption we obtain that M is sequence-saturated relative to S and σ(**M, S**α) is the minimal change update model of bSα(U). Also, by Proposition 97, N is sequence-saturated relative to S and σ(**N, S**α) is the MKNF model of bSα(Un). Furthermore, by Corollary 95, σ(M′, Sα) = σ(M ⊕ **N, S**α) = σ(M, Sα) ⊕ σ(N, Sα) ,