the criteria for a given trial. Deriving all the consequences of a knowledge base to answer a query about a given shipment or patient would be impractical.

In this section we describe the algorithms and the design of *CDF-Rules***, a goaldriven implementation for Hybrid MKNF Knowledge Bases under the Well-Founded**
Semantics that minimizes the computation to the set of individuals that are relevant to a query. *CDF-Rules* **makes use of XSB's tabled SLG Resolution (Chen and Warren 1996)**
for the evaluation of a query, together with tableaux mechanisms supported by CDF
theorem prover to check entailment on the ontology. *CDF-Rules* **is tuned for Type-1**
ontologies, and thereby is also compatible with Type-0 ontologies. For the description of the solution, we assume that the reader has a general knowledge of tabled logic programs (cf. e.g. (Swift and Warren 2012)).

## 4.1 A Query-Driven Iterative Fixed Point

At an intuitive level, a query to *CDF-Rules* **is evaluated in a relevant (top-down** like) manner through SLG resolution, until the selected goal is a literal l **formed**
over a DL-atom. At that point, in addition to further resolution, the ontology also uses tableau mechanisms to derive l. However, as a tableau proof of l **may require** propositions (literals) inferred by other rules, considerable care must be taken to integrate the tableau proving with rule-based query evaluation.

In its essence, a tableau algorithm decides the entailment of a formula ϕ **w.r.t. an**
ontology O **by trying to construct a common** *model* for ¬ϕ and O**, sometimes called** a *completion graph* **(cf. e.g. (Schmidt-Strauss and Smolka 1990)). If such a model** can not be constructed, O |= ϕ; otherwise O does not entail ϕ**. Similar to other** description logic provers, the CDF theorem prover attempts to traverse as little of an ontology as possible when proving ϕ**. As a result, when the prover is invoked on**
an atom A**, the prover attempts to build a model for the underlying individual(s)**
to which A **refers, and explores additional individuals only as necessary.**
For our purposes, given the particular interdependence between **the rules and**
the ontology in *MKNF*W F S **, the prover must consider the knowledge inferred by**
the rules in the program for the entailment proof, as a DL-atom can **be derived by**
rules, which in turn may rely on other DL-atoms entailed by the ontology. Thus, a query to a DL-atom p(o), iteratively computes a (sub-)model for o**, deriving at each** iteration new information about the roles and classes of o**, along with information** about other individuals related to o **either in the ontology (via CDF's tableau** algorithm) or in the rules (via SLG procedures) until a fixed point is reached.

We start by illustrating the special case of positive knowledge bases **without**
default negation in the rules.