A Goal-Directed Implementation of Query Answering for Hybrid MKNF 17 an outer fixed point has in fact been reached. Since c(object**) is in the model of the** final iteration, the query c(X) succeeds for X = **object**.

The procedure to compute a lazily invoked iterative fixed point over a **DLsafe MKNF Hybrid Knowledge Base is summarized in Figure 2 using predicates**
that are described in detail in Section 4.2. In each inner iteration, the tabled predicate known/**3 is used to derive knowledge from the rules component, while** allModelsEntails/**3 infers knowledge from the ontology via tableau proofs. Within** rules evaluated by known/3, the default negation of a DL-atom A **is obtained by the** predicate dlnot(A), which succeeds if A **was not proven in the last outer iteration.**
The predicates def inedClass/2 and def inedRole/**3 are used to obtain the relevant**
classes and roles defined for a given individual. We assume that these **predicates are** defined explicitly by the compiler or programmer, but they can also be **inferred via**
the DL-safe restriction 9**. Regardless of whether inference is used, whenever a role**
is encountered for an individual, a check is made to determine whether the related individual Individual1 **is already in the list of individuals in the fixed point, and**
Individual1 **is added if not.**
In order to compute *MKNF*W F S **the algorithm shown in Figure 2 must create two**
different sets (cf. Definition 7): a credulous set, T U**, containing the atoms that are**
true or undefined corresponding to application of the operator Γ′K **; and a skeptical**
set, T , of the atoms that are true corresponding to ΓK **(Definition 6). The iterations in Figure 2 capture the construction of these sets in the following manner. The**
first iteration of OutIter in known(T erm, OutIter, InIter) (where OutIter **= 0)**
corresponds to the first step of computation of the set T U**, whereas the second**
iteration corresponds to the second step of computation of the set T . As a consequence, iterations where OutIter **is indexed with an even number are monotonically** decreasing T U iterations, while iterations indexed with an odd number are monotonically increasing T **iterations. By making use of this property, the algorithm of**
Figure 2 ensures that the fixed point will only be achieved in T U **iterations. This**
way, Query is true if known(Query, OuterF inal −1, InnerF inal**) holds. If this is not**
the case, then Query is undefined if known(Query, OuterF inal, InnerF inal**) holds,**
and Query **is false otherwise.**

## 4.2 Implementing Mknfw F S **Components**

We now describe the various predicates in the algorithm of Figure 2, including the manner in which the rule and ontology components exchange knowledge, and how the fixed point is checked.