right7) and the query **third**(X):
K third(X) ← p(X), K **second**(X).

K f irst(callback). F irst ⊑ **Second**
p(**callback**).

The query resolves against the rule for third(X), leading to the goals p(X**) and**
K second(X). The predicate p, although not a DL-atom, assures DL-safety, restricting the application of the rules to known individuals. The call p(X**) returns true for**
X = callback. Accordingly, the next subgoal is K second(callback**) which depends**
on the DL-atom second(callback), corresponding in the ontology to the proposition Second**. At this point, the computation calls the CDF theorem prover which**
starts to derive a model for all the properties of the individual callback**. Yet in this** computation, the proposition Second **itself depends on a predicate defined in the** rules - F irst. It can thus be seen that the evaluation of the query third(**callback**) must be done iteratively - the (instantiated) goal third(callback**) should suspend** (using tabling) until second(callback) is resolved. Furthermore, second(**callback**)
needs first to prove f irst(callback**) from the rules. In general, goals to DL-atoms**
may need to suspend in order to compute an iterated fixed point, after which they may either succeed or fail.

To formalize the actions in Example 3 on the special case of definite programs, we start by considering the computation for all individuals (i.e. temporarily disregarding the relevance of individuals, as discussed above).

## Definition 8

Let K = (O,P) be a DL-safe hybrid MKNF knowledge base, where P does not contain default negation. Let I **be a fixed set of individuals. The function** *Tableau*(O) computes for a theory O the entailments of O for I, disregarding the rules component. The function SLG(P**) computes via tabling the set of DL-atoms true in the**
minimal model of P for a set of individuals, I**, disregarding the ontology component.** The model is obtained as the union of the least fixed point of the sequences:

$R_{0}=$ SLG(P)  $R_{1}=$ SLG(P U D${}_{0}$)  $\bullet$  $R_{n}=$ SLG(P U D${}_{n}$-1)
D0 = T ableau(O) R0 = SLG(P)
D1 = T ableau(O ∪ R0) R1 = SLG(P ∪ D0)
$D_{0}=Tableau(\mathcal{O})$  $D_{1}=Tableau(\mathcal{O}\cup R_{0})$  $\dashv$  $D_{n}=Tableau(\mathcal{O}\cup R_{n-1})$
Dn = T ableau(O ∪ Rn−1) Rn = SLG(P ∪ Dn−1)
Definition 8 resembles Definition 4 of the operator TK **in Section 2. In fact, the**
Ri sequence is similar to the RK(S**) operator which collects new conclusions from**
the rules, whereas the Di sequence is similar to the DK(S**) operator which collects**
new conclusions from the ontology. Rather than starting with the empty set of conclusions from the rules, as is the case for TK of Definition 4, here the Ri **sequence**