respect to this language but we do not stress this fact in the definitions. So instead of defining an "MKNF formula of L**", we simply define an "MKNF formula", leaving** out the words "of L**". Similarly, instead of defining an "MKNF structure over** L", we simply define an "MKNF structure", leaving out the words "over L**". Other** definitions follow this pattern as well.

Furthermore, while in the definitions the notions are defined with their full names
(e.g. "MKNF language", "MKNF formula", . . . ), further in the text **we occasionally**
drop the word "MKNF". We believe these simplifications do not cause any confusion while significantly improving the readability of the text.

We continue with the definition of an MKNF formula:
Definition 2.2 (**MKNF Formula**) A term is a variable or a constant. A first-order atom **is every expression of the** form

## P(T1, T2**, . . . , T**N)

where P is a predicate symbol of arity n and each ti**is a term.**
The set of MKNF formulas **is the smallest set satisfying the following conditions:**
1. Every first-order atom is an MKNF formula.

2. If φ, ψ are MKNF formulas and x is a variable, then ¬φ, (φ ∧ ψ**), (**∃x : φ),
K φ and not φ **are also MKNF formulas.**
Where it doesn't cause confusion, the parenthesis are removed for the sake of readability. Furthermore, (φ∨ψ), (φ ⊃ ψ), (φ ⊂ ψ**), (**φ ≡ ψ), true, false and (∀x : φ**) are**
used as shortcuts for ¬(¬φ ∧ ¬ψ), (¬φ ∨ ψ), (φ ∨ ¬ψ), (φ ⊃ ψ) ∧ (φ ⊂ ψ), (p ∨ ¬p), (p ∧ ¬p) and ¬(∃x : ¬φ), respectively, where p **is a fixed ground first-order atom**
from the language.1 An MKNF formula of the form K φ is called a modal K-atom**, and a formula**
of the form not φ is called a modal not-atom; collectively, modal K- and notatoms are called modal atoms. An MKNF formula φ is a sentence **if it has no**
free variable occurences; φ is open **if all its variable occurences are free;** φ is ground if it does not contain variables; φ is positive if it does not contain occurrences of not; φ is first-order or objective if it does not contain modal operators. By φ[t1/x1, t2/x2, . . . , tn/xn] we denote the formula obtained by simultaneously replacing in φ all free occurences of the variable xi by the term ti **for every**
i ∈ { 1, 2**, . . . , n** }.

A set of MKNF sentences is an MKNF theory**. An MKNF theory has property** X
if all its members do (for instance, an MKNF theory is first-order **if all sentences** inside it are first-order).

Now we can define the semantics of MKNF formulas. We use Herbrand interpretations, assuming that apart from the constants from C **occurring in the formulas,**
the signature contains a coutably infinite supply of constants not occurring in the 1 **As stated in above, we assume that at least one predicate symbol and at least one constant**
symbol exist in the language, from which at least one ground first-order atom can be formed.