Proof See Appendix Appendix D, page 35.

The following proposition relates the hybrid update operator to the **static MKNF**
semantics of hybrid knowledge bases. It gives sufficient conditions for the static and dynamic semantics to coincide. In particular, the sufficient condition **requires that** for any set of consequences S of program P in the context of a model M**, updating** S by A in the context of T **has the same effect as making an intersection of the**
models of S with the models of A and T .

Proposition 4.3 (**Relation to Hybrid MKNF**) Let P be a finite ground program, O = T ∪ A an ontology with TBox T and ABox A and M an MKNF interpretation such that for every subset S **of the set**
{ H∗(r) | r ∈ P ∧ M |= B(r) } **the following condition is satisfied:**

## Mod(S ⊕ T A) = Mod(S ∪ O) .

Then M is an MKNF model of hO,Pi if and only if M **is a minimal change dynamic**
stable model of P ⊕T A.

## Proof See Appendix Appendix D, Page 36.

The precondition of this proposition is satisfied, for example, when predicates appearing in heads of P do not appear in the ontology O**. An important subcase**
of this is when O **is empty because then the proposition implies that the minimal**
change dynamic stable models of P ⊕∅ ∅ are exactly the MKNF models of P**. Since**
the MKNF semantics generalises the stable model semantics (Lifschitz 1991), the minimal change dynamic stable models of P ⊕∅ ∅ **also coincide with the stable**
models of P**. In other words, our operator properly generalises stable models.** Corollary 4.4 (**Generalisation of stable models**) Let P be a finite ground program. Then M is a stable model of P **if and only if** M
is a minimal change dynamic stable model of P ⊕∅ ∅.

## Proof See Appendix Appendix D, Page 37.

Turning to relations with the minimal change update operator, we show that updating any logic program that can be equivalently translated into first-order logic has the same effect as updating the translated first-order theory using the minimal change update operator. Hence, our update operator generalises the classical minimal change update operator. Proposition 4.5 (**Generalisation of the minimal change update operator** ) Let P be a finite ground program containing only facts, T a TBox, A **a sequence** of ABoxes and M an MKNF interpretation. Then M **is a minimal change dynamic**
stable model of P ⊕T A if and only if M **is a minimal change update model of**
SP ⊕T A where SP = { p | K p ∈ P }.