Query-driven Procedures for Hybrid MKNF Knowledge Bases · 29

![0_image_0.png](0_image_0.png)

NonMarried = -Married (8) -Married (9) -Spouse.T = Married (10) (SDpause.(Michelle))(Bill) (11) NonMarried(x) - notMarried(x) (12) discount(x) $\leftarrow$ notHighRisk(x) (13)
First, note that TBox and ABox information are each distributed over both the DL KB and the rules. Figure 2 shows the final forest for this evaluation, where elements are marked in the order they are created. The initial forest for the evaluation consists of node 1 only. Given the selected literal of node 1, discount(Bill),
we can only apply Program Clause Resolution**, so we use rule (13) to produce**
node 2, followed by New Subgoal **to produce node 3. No rules are applicable for** node 3, HighRisk(Bill), but an Oracle Resolution **operation can be applied**
to derive from axioms (8) and (9) that if NonMarried(Bill**) can be proven (node**
4), then this suffices to prove HighRisk(Bill). Then, via a New Subgoal **operation, node 5 is obtained. For the selected literal in node 5,** NonMarried(Bill),
Program Clause Resolution produces node 6 from (12) and **New Subgoal**
produces node 7. The selected literal of node 7, Married(Bill**), is not the head**
of a rule, so the only possibility is to use Oracle Resolution**, and the answer**
Married(Bill**) is derived from axioms (10) and (11). Using this answer, the tree**
for Married(Bill) can be early completed and a Negative Return **operation**
produces node 10. The tree for NonMarried(Bill**), which does not have an answer,** must be completed (step 11), and the same holds for HighRisk(Bill**) (step 12).**
Once this occurs, a Negative Return **operation is enabled to produce node 13.**
The evaluation in the example illustrates two main points. First, the evaluation makes use of classical negation in the ontology along with closed world **negation in** the rules. Second, the actions of the DL part and the program part are interleaved, with the program "calling" the oracle by Oracle Resolution**, and the oracle**
"calling" the program back with the answers of that operation.

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