then Program Clause Resolution and Oracle Resolution are not distinguishable. Thus, we can consider that Oracle Resolution **is a syntactic variant**
of Program Clause Resolution. The same holds for New Subgoal **and the**
treatment of default negated atoms not S that create a tree with root S **and those**
special literals not NH(ti**) that may allow us to create a tree with root** ¬H(ti):
both its children are not distinguishable and only one of the two is applicable in each case. Thus, confluence of SLG(O) **follows directly from confluence of SLG**
(see Theorem 5.7 of [Chen and Warren 1996]).

The above theorem is also helpful to prove that SLG(O) **is a correct query**
procedure for MKNFW F **and terminates within the same complexity bounds as the**
semantics defined in [Knorr et al. 2011]. First, we show that SLG(O) **coincides**
with MKNFW F **. Intuitively, what we have to show is that the well-founded MKNF**
model, as presented in Section 2 and based on the computation presented in Section 3, coincides with the interpretation IF induced by the final forest Fn **for some query**
q to Kdin all the ground literals involved in the query.18 **We can further simplify**
that by showing, for each literal L appearing in KdG, that L ∈ MW F **(Definition 2.16)**
if and only if L ∈ IF with ground query q = L and Fn for some n**. Note that this**
correspondence also holds for atoms and classically negated atoms **only appearing**
in the ontology.

Theorem 5.3 Let Kdbe a doubled Hybrid MKNF knowledge base, and IF the interpretation induced by the final forest F of an SLG(O) evaluation of Kd**for a**
ground query q = L where L is a literal or a classically negated atom. **SLG(**O)
resolution is sound and complete w.r.t. MW F , which is obtained from Pdω and Ndω, i.e.,
—for L ∈ KA(KdG):
—L ∈ Pdω if and only if L ∈ IF and
—L
d 1 6∈ Ndω if and only if L = notL
d 1 ∈ IF .

—for L 6∈ KA(KdG): O ∪ Pdω |= L or Od ∪ Pdω |= L **if and only if** L ∈ IF .

Proof. (Completeness): We show by induction on n **that**
—for L ∈ KA(KdG), if L **is a positive literal, then** L ∈ Pdn implies that L ∈ IF **; and**
if L = notL
d 1**is a negative literal, then** L
d 1 6∈ Ndn implies that notL
d 1 ∈ IF
—for L 6∈ KA(KdG), if O ∪ Pdn |= L or Od ∪ Pdn |= L **then** L ∈ IF .

The induction base holds immediately, for L ∈ KA(KdG**), since** Pd 0**is empty and**
Nd 0 contains all literals appearing in KA(KdG). For L 6∈ KA(KdG**), we obtain that**
O |= L or Od|= L, so we can create a tree L : − | L and with **Oracle Resolution**
an answer L : − |**, which shows** L ∈ IF .

(Induction Hypothesis 1) Now suppose the claim holds for n**. We have to show**
the induction step for n + 1. For L ∈ KA(KdG), let L **be a positive literal, and**
suppose that L ∈ Pdn+1 but L 6∈ Pdn **(otherwise the claim would immediately follow**
by the induction hypothesis). Therefore, L ∈ ΓKdG

(Ndn
) and so L ∈ TKdG//′Ndn

↑ ω 18**Without loss of generality, we can restrict that statement to ground queries, a non-ground query**
would simply require to check all the ground instances.

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