Towards Closed World Reasoning in Dynamic Open Worlds 17 KM 6: If φ ⋄ ψ1 implies ψ2 and φ ⋄ ψ2 implies ψ1, then φ ⋄ ψ1 **is equivalent to**
φ ⋄ ψ2.

KM 7: If for each atom p either φ implies p or φ implies ¬p**, then (**φ⋄ψ1)∧(φ⋄ψ2)
implies φ ⋄ (ψ1 ∨ ψ2).

KM 8: (φ1 ∨ φ2) ⋄ ψ **is equivalent to (**φ1 ⋄ ψ) ∨ (φ2 ⋄ ψ).

In order to examine these postulates in our setting, we restrict our attention to a finite propositional language. In order to interpret the postulates in our setting, we need to define the semantics of a number of notions used in them. Let P,P1,P2 be programs, T a TBox and α, α1, α2 **be propositional formulae representing ABox**
updates. We need to discuss and define, at least:
1. When does P ⊕T α1 imply α2**? (used in KM 1 and KM 6)**
2. When does P imply α**? (used in KM 2 and KM 7)**
3. When is P1 ⊕T α equivalent to P2**? (used in KM 2)**
4. When is P **satisfiable? (used in KM 3)**
5. When is P ⊕T α **satisfiable? (used in KM 3)**
6. When is P1 equivalent to P2**? (used in KM 4)**
7. When is P1 ⊕T α1 equivalent to P2 ⊕T α2**? (used in KM 4 and KM 6)**
8. What is the semantics of (P ⊕T α1) ∧ α2**? (used in KM 5)**
9. What is the semantics of (P ⊕T α1) ∧ (P ⊕T α2**)? (used in KM 7)**
10. What is the semantics of P1 ∨ P2**? (used in KM 8)**
Most of these questions can be answered in multiple different ways while some of them are hard to provide answers to at all. In the following, we suggest ways of answering most of these questions and then analyse whether our operator satisfies the corresponding postulates.

Question 1. can be answered using the consequence relation from Def. **3.5. A**
similar consequence relation can be defined using stable models to answer question 2. A simple answer to question 3. is to say that P1 ⊕T α is equivalent to P2 **if the** set of minimal change dynamic stable models of P1⊕T α **is equal to the set of stable**
models of P2. Regarding questions 4. and 5., we can say that P **is satisfiable if it**
has at least one stable model and P ⊕T α **is satisfiable if it has at least one minimal**
change dynamic stable model. Question 6. can be answered similarly as **question**
3. by comparing the sets of minimal change dynamic stable models of P ⊕T α1 and P ⊕T α2**. Finally, question 7. can be answered by comparing the sets of stable**
models of P1 and P2 **or by using strong equivalence (Lifschitz et al. 2001). Providing**
reasonable answers to the remaining questions requires more investigation, so, for now, we do not further examine postulates KM 5, KM 7 and KM 8.

Turning to the rest of the postulates, we note that our operator **adheres to KM 1,**
which was proved in Proposition **4.1. The same is not the case with postulate KM 2,**
as shown by the following counterexample. Consider the program P : p ← not q. r ← q, not r.

$5\quad\;9$, $\pi$
$$r\gets p.$$
$$q\leftarrow n o t\,p.$$

 $\text{imal S5model}$ i. 
q ← not **p. r** ← p.
(7)
and an update α = r. The only stable model of P is the maximal S5 model M of