36 M. Slota and J. Leite and T. Swift Corollary 61 Let U be a splitting set for a hybrid knowledge base K and **M, X, Y** be MKNF interpretations such that X[U] = M[U]and Y
[P\U] = M[P\U]. Then:
M |= π(K) ⇐⇒ X |= π(bU (K)) ∧ Y |= π(eU (K, X)) .

Proof Proposition 59 for D = D′ = M, E = E′ = X, F = F
′ = Y and G = G′ = X implies that hM, Mi |= π(K) ⇐⇒ hX, Xi |= π(bU (K)) ∧ hY, Y i |= π(eU (K**, X, X**)) .

The claim of this corollary now follows from Proposition 51.

Corollary 62 Let U be a splitting set for a hybrid knowledge base K and M, M′**, X, X**′ be MKNF
interpretations such that M |= π(K), M′[P\U] = M[P\U], X[U] = M[U]and X′[U] =
M′[U]. Then:
hM′, M**i 6|**= π(K) =⇒ hX′, X**i 6|**= π(bU (K)) .

Proof Proposition 59 for D = M, D′ = M′, E = X, E′ = X′, F = F
′ = M, G = G′ = X
implies that hM′, Mi 6|= π(K) **⇐⇒ h**X
′, Xi 6|= π(bU (K)) ∨ hM, Mi 6|= π(eU (K**, X, X**)) .

Furthermore, from Corollary 60 we know that M |= π(eU (K, X)) is always satisfied because M |= π(K). Hence, by Corollary 53, the second disjunct on the right hand side of the above equivalence can be safely omitted and we obtain the claim of this corollary. Corollary 63 Let U be a splitting set for a hybrid knowledge base K and M, M′**, X, Y, Y** ′ be MKNF
interpretations such that M |= π(K), M′[U] = X[U] = M[U], Y
[P\U] = M[P\U]and Y
′[P\U] = M′[P\U]. Then:
hM′, M**i 6|**= π(K) =⇒ hY
′, Y i 6|= π(eU (K, X)) .

Proof Proposition 59 for D = M, D′ = M′, E = E′ = M, F = Y , F
′ = Y
′, G = G′ = X
implies that hM′, Mi 6|= π(K) ⇐⇒ hM, Mi 6|= π(bU (K)) ∨ hY
′, Y i 6|= π(eU (K**, X, X**)) .

Furthermore, from Corollary 60 we know that M |= π(bU (K)) is always satisfied because M |= π(K). Hence, by Corollary 53, the first disjunct in the right hand side of the above equivalence can be safely omitted and we obtain the claim of this corollary.

Corollary 64 Let U be a splitting set for a hybrid knowledge base K and M, M′**, X, X**′ be MKNF interpretations such that X[U] = M[U]and X′[U] = M′[U]. Then:
hX
′, X**i 6|**= π(bU (K)) =⇒ hM′, M**i 6|**= π(K) .