formulas. The Herbrand Universe of such a signature is denoted by **∆ and has**
the property C ⊆ **∆. If not stated otherwise, we assume that one fixed Herbrand**
Universe ∆ with these properties is used as the universe for all interpretations.

Definition 2.3 (**First-Order Interpretation and Model**)
A first-order interpretation I is a relational structure that contains for every predicate symbol P ∈ P of arity n **a relation** P
I ⊆ ∆n**. The set of all first-order**
interpretations is denoted by I.

Each first-order interpretation determines a unique truth assignment to all firstorder sentences. The satisfiability of a first-order sentence φ in I **is defined inductively as follows:**

1
◦If φ is a ground first-order atom P(c1, c2, . . . , cn), then φ is true in I **if and**
only if (c1, c2**, . . . , c**n) ∈ P
I;
2
◦If φ is a first-order formula of the form ¬ψ, then φ is true in I **if and only if**
ψ **is not true in** I;
3
◦If φ is a first-order formula of the form φ1 ∧φ2, then φ is true in I **if and only**
if φ1 is true in I and φ2 **is true in** I;
4
◦If φ is a first-order formula of the form (∃x : ψ), then φ is true in I **if and**
only if ψ[c/x] is true in I **for some constant** c ∈ ∆.
The fact that φ is true in I is denoted by I |= φ. A formula φ is false in I **if and** only if it is not true in I, denoted by I 6|= φ. For a first-order theory S **we say that** S is true in I, denoted by I |= S, if I |= φ for each φ ∈ S. Otherwise, S **is false in**
I**, denoted by** I 6|= S.

If I |= φ, then we say that I is a model of φ. Similarly, if I |= S, then I is a **model**
of S. The set of all models of φ **is denoted by** mod(φ**). The set of all models of** S is denoted by mod(S).

The satisfiability of MKNF formulas is defined with respect to MKNF structures.

Definition 2.4 (**MKNF Structure**)
An MKNF structure is a triple hI, M, Ni where I **is a first-order interpretation and**
M, N **are sets of first-order interpretations.**2 Every MKNF structure has three components. The first is a first-order interpretation used to interpret the objective parts of a formula. The second and third are sets of first-order interpretations used to interpret the parts **of a formula under the**
K and not **modality, respectively.**
Definition 2.5 (**MKNF Satisfiability**)
Let hI, M, Ni **be an MKNF structure. The satisfiability of an MKNF sentence** φ in hI, M, Ni **is defined inductively as follows:**
1
◦If φ is a ground first-order atom P(c1, c2, . . . , cn), then φ is true in h**I, M, N**i if and only if (c1, c2**, . . . , c**n) ∈ P
I;

```
2
 In difference to (Motik and Rosati 2007), we allow for empty M, N in this definition as later on
 it will be useful to have satisfiability defined even for this marginal case. However, the empty
 set is still not considered an MKNF interpretation as can be seen further in Definition 2.6

```
