theorem then warrants that stable models of P consist of a union of stable models of each of its layers after appropriate reductions.

In the following we generalise these notions to Hybrid MKNF Knowledge Bases (Motik and Rosati 2007).

The first definition establishes the notion of a splitting set in this context.

Definition 4 *(Splitting Set*)
A splitting set for a hybrid knowledge base K = hO,Pi is any set of predicate symbols U ⊆ P such that 1. For every ontology axiom φ ∈ O, if pr(φ) ∩ U 6= ∅, then pr(φ) ⊆ U. 2. For every rule r ∈ P, if pr(H(r)) ∩ U 6= ∅, then pr(r) ⊆ U;
The set of ontology axioms φ ∈ O such that pr(φ) ⊆ U is called the *bottom of* O
relative to U and denoted by bU (O). The set of rules r ∈ P such that pr(r) ⊆ U is called the bottom of P *relative to* U and denoted by bU (P). The hybrid knowledge base bU (K) = hbU (O), bU (P)i is called bottom of K *relative to* U.

The set tU (O) = O \ bU (O) is the top of O *relative to* U. The set tU (P) = P \ bU (P)
is the top of P *relative to* U. The hybrid knowledge base tU (K) = htU (O), tU (P)i is the top of K *relative to* U.

Note that instead of defining a splitting set as a set of atoms, as was done in the case of propositional logic programs, we define it as a set of predicate symbols. By doing this, the set of ground atoms with the same predicate symbol is considered either completely included in a splitting set, or completely excluded from it. While this makes our approach slightly less general than it could be if we considered each ground atom individually, we believe the conceptual simplicity is worth this sacrifice. Also, since all TBox axioms are universally quantified, in many cases we would end up adding or excluding the whole set of ground atoms with the same predicate symbol anyway.

Next, we need to define the reduction that makes it possible to properly transfer information from an MKNF model of the bottom of K, and use it to simplify the top of K.

Definition 5 *(Splitting Set Reduct*)
Let U be a splitting set for a hybrid knowledge base K = hO,Pi and X ∈ M. The splitting set reduct of K relative to U and X is a hybrid knowledge base eU (K, X) =
htU (O), eU (P, X)i, where eU (P, X) consists of all rules r
′such that there exists a rule r ∈ tU (P) with the following properties: X |= π({ L ∈ B(r) | pr(L) ⊆ U }), H(r
′) =
H(r), and B(r
′) = { L ∈ B(r) | pr(L) ⊆ P \ U }.

This leads us to the notion of a solution to K w.r.t. a splitting set U.

Definition 6 (*Solution w.r.t. a Splitting Set*)
Let U be a splitting set for a hybrid knowledge base K. A solution to K *w.r.t.* U is a pair of MKNF interpretations h**X, Y** i such that X is an MKNF model of bU (K) and Y is an MKNF model of eU (K, X).

The splitting theorem now ensures that solutions to K w.r.t. any splitting set U are in one to one correspondence with the MKNF models of K.