If there exists the greatest M ∈ M such that M |= T , then we denote it by mod(T ).

For all other sets of formulae mod(T ) stays undefined.

If M is an MKNF interpretation (i.e. M is nonempty and M ∈ M), we say M is
- an *S5 model of* T if M |= T ;
- an *MKNF model of* T if M is an S5 model of T and for every MKNF interpretation M′ ) M there is some I
′ ∈ M′and some φ ∈ T such that hI
′, M′, M**i 6|**= φ.

We say a set of MKNF formulae T is *MKNF satisfiable* if an MKNF model of T exists; otherwise it is *MKNF unsatisfiable*. The S5 (un)satisfiability is defined analogously by considering S5 models instead of MKNF models. For a sentence φ, we write M |= φ if and only if M |= { φ }; otherwise we write M 6|= φ. Also, mod(φ), S5 models of φ, MKNF models of φ, MKNF (un)satisfiability and S5 (un)satisfiability of φ are defined as mod({ φ }), S5 models of { φ }, MKNF models of { φ }, MKNF (un)satisfiability of { φ }
and S5 (un)satisfiability of { φ }, respectively.

Let U ⊆ P be a set of predicate symbols, I, J ∈ I and M, N ∈ M. We define the restriction of I to U as I
[U] = { p ∈ I | pr(p) ⊆ U } and the *restriction of* M to U as M[U] =I
[U] I ∈ M	. We say that I *coincides with* J on U if I
[U] = J
[U]and that M
coincides with N on U if M[U] = N[U].

Description Logics. Description Logics (Baader et al. 2003) are (usually) decidable fragments of first-order logic that are frequently used for knowledge representation and reasoning in applications. Throughout the paper we assume that some Description Logic is used to describe an ontology, i.e. it is used to specify a shared conceptualisation of a domain of interest. Basic building blocks of such a specification are *constants*, representing objects (or individuals), *concepts*, representing groups of objects, and *roles*, representing binary relations between objects and properties of objects. Typically, an ontology is composed of two distinguishable parts: a TBox specifying the required terminology, i.e. concept and role definitions, and an ABox with assertions about constants.

Most Description Logics can be equivalently translated into function-free first-order logic, with constants represented by constant symbols, atomic concepts represented by unary predicates and atomic roles represented by binary predicates. We assume that for any DL axiom φ, ζ (φ) denotes such a translation of φ. We also define pr(φ) as pr(ζ (φ)).

Generalised Logic Programs. We consider ground logic programs for specifying nonmonotonic domain knowledge. The basic syntactic blocks of such programs are ground atoms. A *default literal* is a ground atom preceded by ∼. A *literal* is either a ground atom or a default literal. As a convention, due to the semantics of rule updates that we adopt in what follows, double default negation is absorbed, so that ∼∼p denotes the atom p.

A *rule* r is an expression of the form L0 ← L1, L2**, . . . , L**k where k is a natural number and L0, L1**, . . . , L**k are literals. We say H(r) = L0 is the *head of* r and B(r) =
{ L1, L2**, . . . , L**n } is the *body of* r. A rule r is a *fact* if its body is empty; r is *positive* if its head is an atom. A *generalised logic program* (GLP) P is a set of rules. The set of predicate symbols occurring in a literal L, set of literals B and a rule r is denoted by pr(L), pr(B)
and pr(r), respectively. An interpretation I is a *stable model* of a GLP P if I
′ = least(P ∪
{ ∼p | p is an atom and p /∈ I }), where I
′ = I ∪ { not p | p is an atom and p /∈ I } and least(·) denotes the least model of the program obtained from the argument program by replacing every default literal ∼p by a fresh atom not p.