(a) The first simplification case corresponds exactly to **Negation Failure**,
only here the failure occurs in Delays **and the failed literal may be positive** or negative.

(b) The second simplification case corresponds exactly to **Negation Success**,
only now the success occurs in Delays **and the successful literal may be** positive or negative.

(7) Oracle Resolution: A new child is created for the root S ← | S **by means**
of the oracle. If the returned list of goals is empty, then the oracle **allows us**
to derive the root directly, and O ∪ IFn |= L or Od ∪ IFn |= L**. In this case,**
if L is a positive literal with L = S, then L ∈ IFn+1. If L ∈ KA(KdG**), then**
L ∈ Pdω
, since the operator DKdG

together with all L
′ ∈ IFn
**, for which** L
′ ∈ Pdω holds by the induction hypothesis, allows us to derive L. If L 6∈ KA(KdG**), then**
O ∪ Pdω |= L or Od ∪ Pdω |= L **holds since we have that, for all** L
′ ∈ IFn
,
L
′ ∈ Pdω **holds by the induction hypothesis. Alternatively, if the list of goals**
is not empty, then L ∈ IFn+1 implies L ∈ IFn**, and the property holds by the**
induction hypothesis.

(8) Completion: This operation only affects IF if some A is in the ground instantiation of a completely evaluated literal in F and A **is not in the ground**
instantiation of any answer in a tree in F. In other words, this operation introduces notL
′to IF . In particular, consider L = notL
d 1 **as a negative literal**
and L ∈ IFn+1 **. Thus, the tree for** L
d 1 **does not contain any answer but also no**
further operation can be applied, i.e., in each child, there is (at least) **one literal** that either can not be resolved or it is failed. This matches the condition of the greatest unfounded set and we obtain that L
d 1 6∈ Ndω
. For all other cases, if L ∈ IFn+1, then L ∈ IFn**, and the property holds by the induction hypothesis.**
(9) Answer Completion: This operation may affect IF **by adding failure nodes**
as children to conditional answers. Assume that one such answer occurs within some tree with root S ← S in Fn. In such a case, S **may become false in**
IFn+1 but was not false in IFn**. However, the notion of an answer that is**
not supported (Definition 4.13) captures the definition of an element of an unfounded set: in this case literals in the unfounded set may be in the **Delays**
of an answer. As with the case of Completion, we have that for any L **in the**
ground instantiation of S, L
d 6∈ Ndω
. For all other cases, if L ∈ IFn+1**, then**
L ∈ IFn
**, and the property holds by the induction hypothesis.**
We conclude that soundness holds.

Given the soundness of MKNFW F **with respect to the semantics of MKNF knowledge bases of [Motik and Rosati 2010], it follows easily from [Knorr et al. 2011] that:**
Corollary 5.4 Let K be a Hybrid MKNF knowledge base and L a literal that appears in KdG. If L ∈ IF (L = notL
d 1 ∈ IF respectively), where IF **is induced by**
the forest F of an SLG(O) evaluation of KdG for query q = L, then L (notL1 respectively) is derivable from all two-valued MKNF models of K.

In addition to the interpretation of the final forest IF **being sound with respect to**
the 2-valued MKNF model, the conditional answers in F can be seen as a wellfounded reduct of the rules in K**, augmented with conditional answers derived by**
ACM Transactions on Computational Logic, Vol. V, No. N, September 2018.