Proof. **We show both inclusions from which the equality follows.**
KA(Kd) \ Nd i+1 ⊆ UKd (Pd i
,KA(Kd) \ Nd i
): Let H ∈ KA(Kd) \ Nd i+1**. Then** H 6∈
Nd i+1**, i.e.,** H 6∈ ΓKd (Pd i
) and H 6∈ lfp(TKd//′Pd i

). Thus, two conditions hold. First, for all rules of the form H ← B+ ∧ B− in P
d, there is at least one A ∈ B+ **with** A ∈
KA(Kd) \ Nd i+1, or at least one not B ∈ B− **with** B ∈ Pd i
, or OBO,Pi |= ¬H1(t~H1)
and not H1(tH~1) ∈ B−**, where** H = Hd 1
(tH~1**). Second, neither** OBO,Nd i+1 |= H
nor OBOd,Nd i+1 |= H **holds. The first condition corresponds exactly to (Ui) of**
Definition 3.9 w.r.t. (Pd i
,KA(Kd) \ Nd i
). We derive from the second condition that, for all S with S ⊆ KA(Kd) on which H depends, there is at least one atom A **such**
that OBO,S\{A} 6|= H, respectively OBOd,S\{A} 6|= H**, and** A in KA(Kd)\Nd i+1**. This**
matches condition (Uii) (resp. condition (Uiid**) of Definition 3.9 w.r.t. (**Pd i
,KA(Kd)\
Nd i
), and we conclude that H ∈ UKd (Pd i
,KA(Kd) \ Nd i
).

UKd (Pd i
,KA(Kd) \ Nd i
) ⊆ KA(Kd) \ Nd i+1**: Let** H ∈ UKd (Pd i
,KA(Kd) \ Nd i
). Then H **occurs in the greatest unfounded set w.r.t. (**Pd i
,KA(Kd) \ Nd i
). It follows from Definition 3.9 that H 6∈ Nd i+1**. Consequently,** H ∈ KA(Kd) \ Nd i+1.

We can now show the correspondence between atoms of K **in the fixed point of**
Definition 2.13 and those of Kd**in the fixed point of Definition 3.7.**
Proposition 3.11 Let K = (O,P) **be a ground Hybrid MKNF knowledge base.** Then the following holds:
—A ∈ Pω **if and only if** A ∈ Pdω.

—B 6∈ Nω **if and only if** Bd 6∈ Ndω
.

Proof. We show by induction on n **that two conditions hold.**
(i) A ∈ Pn **if and only if** A ∈ Pdn
(ii) B 6∈ Nn **if and only if** Bd 6∈ Ndn This is sufficient since the grounded knowledge base is finite, which means that the iteration is finite and stops for some natural number n**, i.e., the two fixpoints** coincide on the relevant atoms as in (i) and (ii).

The base case for n = 0 is straightforward since P0 and Pd 0 are empty while N0 and Nd 0 **both contain their entire Herbrand base.**
(1) So, suppose that (i) and (ii) hold for n and let A ∈ Pn+1 and B 6∈ Nn+1.

We show that A ∈ Pdn+1 and Bd 6∈ Ndn+1**. The other direction of the equivalence**
follows from an identical argument.

```
(i) First, suppose that A ∈ Pn+1 but A 6∈ Pn (otherwise we obtain the result
  by the induction hypothesis (1) immediately). We show that A ∈ Pdn+1. If
  A ∈ Pn+1, then A ∈ ΓK(Nn), by Definition 2.13, and, thus, A ∈ lfp(TK/Nn
                                                                             
                                                                             ) by
  Definition 2.12. So A ∈ TK/Nn
                                 
                                  ↑ m for some m and we show by induction on
  m that A ∈ TKd//′Nn
                        
                         ↑ m (2), which implies that A ∈ Pdn+1. The base case
  for m = 0 holds immediately. Assume the claim (2) holds for m, we show it
  for m + 1. Suppose that A ∈ TK/Nn
                                       
                                        ↑ (m + 1) then A ∈ TK/Nn
                                                                   
                                                                   (TK/Nn
                                                                           
                                                                            ↑ m).
  Then either A ∈ RK/Nn
                           
                           (TK/Nn
                                  
                                   ↑ m) or A ∈ DK/Nn
                                                        
                                                        (TK/Nn
                                                                
                                                                 ↑ m). We start
  with the first case, i.e., there is a rule A ← A1, . . . , An, not B1, . . . , not Bm with
                    ACM Transactions on Computational Logic, Vol. V, No. N, September 2018.

```
