Splitting and Updating Hybrid Knowledge Bases (Extended Version) 59 Lemma 116 Let **U, V** be splitting sets for a (dynamic) hybrid knowledge base K and **X, Y** be MKNF
interpretations such that X is saturated relative to U, Y is saturated relative to V and X
coincides with Y on U ∩ V . Then, eU (eV (K, Y ), X) = eU∪V (K, X ∩ Y ) .

Proof (sketch)
For the ontology part of the hybrid knowledge base this holds because eU (eV (O, Y ), X) = tU (tV (O)) = bP\U (bP\V (O)) = b(P\U)∩(P\V )(O)
= bP\(U∪V )(O) = tU∪V (O) = eU∪V (O, X ∩ Y ) .

For the rule part, we additionally need to observe that on the right hand side, all body atoms with predicate symbol from U are interpreted under X and all body atoms with predicate symbol from V are interpreted under Y , and Lemma 115 guarantees that X ∩ Y coincides with X on U and with Y on V .

Lemma 117 Let **U, V** be sets of predicate symbols, X ∈ M and let K be a dynamic hybrid knowledge base such that pr(K) is a a subset of V . Then, eU (K, X) = eU (K, σ(**X, V** ))
Proof (sketch)
The second argument of eU (·) is used only to interpret body atoms of rules from K,
which by the assumption contain only predicate symbols from V , and by Proposition 36, σ(**X, V** )
[V ] = X[V ].

Lemma 118 Let S be a saturation sequence, M ∈ M be sequence-saturated relative to S and U be a set of predicate symbols. Then σ(**M, U**) is also sequence-saturated relative to S.

Proof (sketch)
Let I
[Sα] ∈ σ(**M, U**)
[Sα]for all α. Then there is some Jα ∈ σ(**M, U**) such that I
[Sα] =
J
[Sα]
α and some Kα ∈ M such that J
[U]
α = K
[U]
α . From these Kα's we can construct a K ∈ M such that K[Sα∩U] = I
[Sα∩U], from which it follows that K[U] = I
[U]. Hence, I ∈ σ(**M, U**).

Lemma 119 Let K = hKiii<n, where Ki = hOi,Pii, be a dynamic hybrid knowledge base that is both O-based and P-based. Then the minimal change update model of hζ (Oi) ∪ Piii<n with the unique dynamic stable model of hPiii<n.

Proof This can be seen easily since in this case Oiis empty and Pi contains only positive facts, so that the dynamic stable model of hPiii<n coincides with the set of all atoms appearing as heads of rules in the programs, and this also coincides with its minimal change update model.