with at least one rule head in P
d**, and** I
+
F = IF \ {not A | not A ∈ IF }**. The**
complete oracle for O, denoted compTO**, is defined by**
compTO(IF , S,L) iff O ∪ I
+
F **∪ L |**= S or O
d ∪ I
+
F **∪ L |**= S
Example 4.9 Consider the Hybrid MKNF knowledge base K **containing** O.

## C(A) C ⊓ F ⊑ E

Assume that IF **is empty, and that there is at least one rule whose head unifies** with F(a). We query for E(a). In this case, compTO(∅, E(a), {F(a)}**) holds because**
O∪ {F(a)} |= E(a). Thus, deriving F(a**) from the rules would be enough to conclude** that E(a**) is true in the well-founded MKNF model.**
The set O ∪ I
+
F ∪ L **(and likewise** Od ∪ I
+
F ∪ L**) may be inconsistent even though**
the well-founded MKNF model of K **exists. Consequently, such a complete oracle** potentially allows us to obtain a large number of entailments that are eventually useless to derive S if K **is MKNF-consistent.** Example 4.10 Consider the Hybrid MKNF knowledge base K **containing** O.

## C(A) C ⊑ ¬D E ⊑ F

Assume that IF is empty and we query for E(a). If O **were extended with** D(a), O
would become inconsistent, so that all statements would be derivable from the extended O, including E(a). Hence compTO(∅, E(a), {D(a)}) holds because **O ∪ {**D(a)}
is inconsistent. However, as K is MKNF-consistent, D(a**) cannot be derived so that** the corresponding tree eventually fails. In Section 5, we provide the definition of a partial oracle which overcomes this lack of efficiency, and upon which concrete oracles can be based.

Complete oracles are applied to define the next SLG(O) **operation, which has**
no correspondence in SLG:
Definition 4.11 (SLG(O) Operations - 3) Let Kd = (O, Od,P
d) be a doubled Hybrid MKNF knowledge base. Given a forest Fn of an SLG(O**) evaluation**
of Kd, Fn+1 **may be produced by:**
(7) Oracle Resolution: Let Fn contain a tree with root node N = S ← |S,
and suppose that **compT**O(IFn
, S, Goals) holds. Assume that N **does not have**
a child Nchild = S ← |**Goals** in Fn.

15 Then add Nchild **as a child of** N.

SLG(O) **also includes an operation that marks a set of trees as complete if the**
corresponding set of literals is completely evaluated. Completed trees can be used in SLG(O) **to simplify other trees and to augment the interpretation associated** with the forest with default negated literals Definition 4.12 A set S of literals in a forest F is completely evaluated **if at least** one of the conditions holds for each S ∈ S
15For that comparison, we consider the sequences Goals **as sets to avoid that one root node has**
several children whose sequences Goals **are merely permutations.**
ACM Transactions on Computational Logic, Vol. V, No. N, September 2018.