Ai ∈ TK/Nn

↑ m and not Bj 6∈ Nn for all i and j**. For each such rule** A ←
A1, . . . , An, not B1, . . . , not Bm in K **there is, according to Definition 3.1, a rule**
A ← A1, . . . , An, not Bd 1, . . . , not Bdm in P
d**. Since, by the induction hypothesis**
(1), we have that Bi 6∈ Nn **if and only if** Bd i 6∈ Ndn **we obtain that each rule in**
K/Nn **has its correspondent in** Kd//′Ndn
. We obtain by the nested induction hypothesis of (2) that A ∈ TKd//′Nn

↑ (m **+ 1). Otherwise,** A ∈ DK/Nn

(TK/Nn

↑
m**) holds, and** A ∈ DKd//′Nn

(TKd//′Nn

↑ m**) is obtained immediately by the**
induction hypothesis (2) and the identical ontologies O contained in Kd and K.

(ii) To prove (ii) we suppose as well that B 6∈ Nn+1 but B ∈ Nn**. We show that**
Bd 6∈ Ndn+1. If B 6∈ Nn+1, then B ∈ UK(Pn,KA(K) \ Nn**). By Definitions 3.9,**
and 3.1, we obtain that B ∈ UKd (Pdn
,KA(Kd) \ Ndn
). Hence, by Lemma 3.10, B 6∈ Ndn+1.

## This Finishes The Proof.

It follows immediately from this proposition that we can use this alternative computation to compute the well-founded MKNF model. Formally we obtain the following theorem, which shows the adapted well-founded MKNF model. Theorem 3.12 Let K = (O,P) **be a ground, MKNF-consistent Hybrid MKNF**
knowledge base and let PdK, NdK ⊆ KA(Kd) **with**
PdK = {A | A ∈ Pdω and A ∈ KA(K)},NdK = {Ad| Ad ∈ Ndω and Ad ∈ KA(Kd)}.

Then MW F = {A | A ∈ P
d K} ∪ {π(O)} ∪ {not A | A
d ∈ (KA(K
d) \ KA(K)) \ NdK}
is the well-founded MKNF model of K.

Proof. **The result is an immediate consequence of Proposition 3.11 and Definition 2.16.**
The two sets PdK and NdK **are just used to remove superfluous atoms, e.g., the** atoms based on doubled predicates for PdK**. We note that for practical purposes we**
also derive from this theorem and Proposition 3.11 that we have to use the new predicates Ad**if we query for negative literals.**
To better illustrate how each of the two computations work, we finish the section with a technical example. Example 3.13 **Consider the knowledge base** K.

Q ⊑ ¬R
p(a) ← not p(a) Q(a) ← R(a) ← not R(a)
We now show how both computation work in this example, yielding (as expected from Proposition 3.11) the same results.

ACM Transactions on Computational Logic, Vol. V, No. N, September 2018.