Towards Closed World Reasoning in Dynamic Open Worlds 27 Lemma B.5 (**Greatest Model of a First-Order Theory**)
For any first-order theory S **it holds that**
mod(S) = { I ∈ I | (∀φ ∈ S)(I |= φ) }
Proof We will prove that MS = { I ∈ I | (∀φ ∈ S)(I |= φ) }
is the greatest set among the sets M ∈ M **with the property** M |= S.

First we need to prove that MS satisfies this property, i.e. that MS |= S**. Take**
some φ ∈ S and I ∈ MS . Then I |= φ and since φ **is first-order, we also obtain** hI, MS, MS i |= φ. This holds for any I ∈ MS**, so** MS |= φ.

Now let M ∈ M be such that M |= S and suppose I ∈ M. Then for every φ ∈ S
we must have hI, M, Mi |= φ and since φ is first-order, this entails I |= φ**. Hence,**
I ∈ MS , so M ⊆ MS**. This fact finishes our proof.**

## B.3 Relevant Part Of An Mknf Interpretation

Definition B.6 (**Predicate Symbols Relevant to a Ground Formula**)
Given a ground MKNF formula φ, we define the set P[φ] of predicate symbols relevant to φ **inductively as follows:**
1
◦If φ is a first-order atom P(c1, c2, . . . , cn**), then** P[φ] = { P };
2
◦If φ is of the form ¬ψ**, then** P[φ] = P[ψ];
3
◦If φ is of the form φ1 ∧ φ2**, then** P[φ] = P[φ1] ∪ P[φ2];
4
◦If φ is of the form K ψ**, then** P[φ] = P[ψ];
5
◦If φ is of the form notψ**, then** P[φ] = P[ψ].

Definition B.7 (**Constant Symbols Relevant to a Ground Formula**)
Given a ground MKNF formula φ, we define the set C[φ] **of constant symbols relevant**
to φ **inductively as follows:**
1
◦If φ is a first-order atom P(c1, c2, . . . , cn), then C[φ] = { c1, c2**, . . . , c**n };
2
◦If φ is of the form ¬ψ**, then** C[φ] = C[ψ];
3
◦If φ is of the form φ1 ∧ φ2**, then** C[φ] = C[φ1] ∪ C[φ2];
4
◦If φ is of the form K ψ**, then** C[φ] = C[ψ];
5
◦If φ is of the form notψ**, then** C[φ] = C[ψ].

Definition B.8 (**Restriction of an MKNF Interpretation**)
Let I ∈ I and M ∈ M. Given a finite set of predicate symbols P′ ⊆ P **and a**
set of constant symbols C′ ⊆ ∆, we define the restriction of I to P′ and C′ as the Herbrand first-order interpretation I
[P′,C′] over the Herbrand Universe C′**that**
interpretes only the predicates from P′**in such a way that**
(c1, c2**, . . . , c**n) ∈ P
I
[P′,C′] ⇐⇒ (c1, c2**, . . . , c**n) ∈ P
I
where P ∈ P′ and c1, c2, . . . , cn ∈ C′. We also define the restriction of M to P′ and C′ as M[P′,C′] =
nI
[P′,C′]I ∈ M
o.