P is a predicate symbol of arity n and ti are terms. An MKNF formula φ is a *sentence* if it has no free variables; φ is *ground* if it does not contain variables; φ is *subjective* if all atoms in φ occur within the scope of a modal operator; φ is *first-order* if it does not contain modal operators. By φ[t/x] we denote the formula obtained by simultaneously replacing in φ all free occurrences of variable x by term t. A set of first-order sentences is a *first-order* theory. We denote the set of all predicate symbols by P. Given a formula φ, we inductively define the *set of predicate symbols relevant to* φ, denoted by pr(φ), as follows:
1
◦If φ is an atom P(t1, t2**, . . . , t**n), then pr(φ) = { P };
2
◦If φ is of the form ¬ψ, then pr(φ) = pr(ψ);
3
◦If φ is of the form φ1 ∧ φ2, then pr(φ) = pr(φ1) ∪ pr(φ2);
4
◦If φ is of the form ∃x : ψ, then pr(φ) = pr(ψ);
5
◦If φ is of the form K ψ, then pr(φ) = pr(ψ);
6
◦If φ is of the form not ψ, then pr(φ) = pr(ψ).

Given a set of formulae T , we define the *set of predicate symbols relevant to* T , denoted by pr(T ), as follows:
pr(T ) = [
φ∈T
pr(φ) .

As in (Motik and Rosati 2007), we only consider Herbrand interpretations in our semantics. We adopt the *standard names assumption*, and apart from the constants used in formulae, we assume our signature to contain a countably infinite supply of constants.

The Herbrand Universe of such a signature is denoted by ∆. The set of all (Herbrand) interpretations is denoted by I. An *MKNF structure* is a triple h**I, M, N**i where I is an interpretation and **M, N** are sets of Herbrand interpretations. The satisfiability of a ground atom p and of an MKNF sentence φ in h**I, M, N**i is defined as follows

$\quad\blacksquare$
$$J_{\mu}\mathbb{P}^{1}(\mathbb{P})$$
hI,M, Ni |= p iff I |= p hI, M, Ni |= ¬φ iff hI,M, N**i 6|**= φ hI, M, Ni |= φ1 ∧ φ2 iff hI,M, Ni |= φ1 and hI,M, Ni |= φ2 hI, M, Ni |= ∃x : φ iff hI,M, Ni |= φ[c/x] for some c ∈ ∆
hI, M, Ni |= K φ iff hJ, M, Ni |= φ for all J ∈ M
hI, M, Ni |= not φ iff hJ, M, N**i 6|**= φ for some J ∈ N
The symbols ∨, ∀ and ⊂ are interpreted as usual. The semantics of MKNF sentences is summarised in the following definition:
Definition 2 *(MKNF Interpretation and MKNF Model*)
An *MKNF interpretation* is a nonempty set of Herbrand interpretations. We also define M = 2Ito be the set of all MKNF interpretations together with the empty set.

Let T be a set of MKNF sentences and M ∈ M. We write M |= T if hI, M, Mi |= φ for every φ ∈ T and all I ∈ M.

4 Otherwise we write M 6|= T .

4 Notice that if M is empty, this condition is vacuously satisfied for any formula φ, so any formula is true in
∅. For this reason, ∅ is not considered an interpretation and only nonempty subsets of M can be models of formulae.