We follow a path similar to how the stable models of normal logic programs were originally defined (Gelfond and Lifschitz 1988), and start by defining how a definite program can be updated by a sequence of ABoxes, and only afterwards deal with programs containing default negation.

As with the least model of a definite logic program, our resulting model is the least fixed point of an immediate consequence operator. Our operator is in a way similar to the usual immediate consequence operator TP **commonly used to draw**
consequences from a logic program P. The crucial difference between TP **and our**
operator is that in the latter, the consequences are subsequently updated by the sequence of ABoxes A **using the classical update operator. Formally:**
Definition 3.1 (**Updating immediate consequence operator** TP⊕T A)
Let P be a finite ground definite program, T a TBox and A **a sequence of ABoxes.**
We define the operator TP⊕T A for any M ⊆ I **as follows**5:

## Tp⊕T A(M) = Mod({ H ∗(R) | R ∈ P ∧ M |= B(R) } ⊕T A)

An important property of an immediate consequence operator is continuity **because it guarantees the existence of a least fixed point and also provides a way**
of computing this least fixed point (using the Kleene Fixed Point Theorem). The TP⊕T A **operator satisfies the condition of continuity:**
Proposition 3.2 (**Continuity of** TP⊕T A)
Let P be a finite ground definite program, T a TBox and A **a sequence of ABoxes.**
Then TP⊕T A **is a continuous function on the complete partial order (**M, ⊇).

## Proof

See Appendix Appendix D, page 34.

Now we can define a minimal change dynamic stable model of P ⊕T A**, where** P
is a definite program, as the least fixed point of TP⊕T A:
Definition 3.3 (**Minimal change dynamic stable model for definite programs**) Let P be a finite ground definite program, T a TBox and A **a sequence of ABoxes.** We say an MKNF interpretation M is a **minimal change dynamic stable model of**
P ⊕T A **if it is the least fixed point of** TP⊕T A.

Notice that for every definite program P and each sequence of ABoxes A, P ⊕T A
has either no minimal change dynamic stable model (when the least fixed point of TP⊕T A **is empty), or exactly one minimal change dynamic stable model.**
In order to deal with default negation in the bodies of rules, we use the GelfondLifschitz transformation which was used to define the stable models **of a normal logic**
program (Gelfond and Lifschitz 1988). We do this by defining the definite program PM **which is the result of performing the Gelfond-Lifschitz transformation on** P –
rules from P with a negative body that is in conflict with M **are discarded, while**
5 Recall that M |= B(r) holds if and only if M is an S5 model of every modal atom in B(r**) (see**
also Def. 2.6).