:- table allModelsEntails /3.

allModelsEntails ( neg ( Atom ) , _OutIter , _InIter ):- !,
/* transform Atom to CDF object identifier and class expression */
/* add individuals to current fixed point list */
( rec_allModelsEntails (Id , CE ) -> fail ; true ).

allModelsEntails ( Atom , _OutIter , _InIter ):-
/* transform Atom to CDF object identifier and class expression */
/* add individuals to current fixed point list */
( rec_allModelsEntails (Id , neg ( CE )) -> fail ; true ).

Fig. 5. Prolog Pseudo-code for **allmodelsEntails/**3 The tableau prover, called by rec allModelsEntails/**2, obtains all information**
inferred by the rules during the previous inner iteration, in accordance with Definition 8. This is addressed via the CDF intensional rules. As discussed in **Section 3,**
the architecture of a CDF instance can be divided into two parts - extensional facts and intensional rules. Extensional facts define CDF classes **and roles as simple** Prolog facts; intensional rules allow classes and roles to be defined by Prolog rules that are outside of the *MKNF*W F S **semantics. In our case, the intensional rules**
support a programming trick to check rule results from a previous iteration. As shown in Figure 6 they convert the CDF form of an ontology axiom into **a 1-ary or** 2-ary predicate, and then check the known/**3 table for a previous iteration using** the predicate *lastKnown/1* **(not shown). If roles or classes are uninstantiated in**
the call from the tableau prover, all defined roles and classes for the individual are instantiated using definedClass/3 or *definedRole/4* **before calling** *lastKnown/1*.

## 4.2.3 Usage

An MKNF Hybrid Knowledge base is defined over a XSB-Prolog knowledge base together with an ontology specified over CDF. In *CDF-Rules* **such a knowledge base**
is written into two files as follows:
- rules.P **– containing the set of MKNF rules and facts. A rule is defined as**
standard Prolog rules as follows:
Head :- A1, ... Ak,known(B1),. . .,known(Bn),dlnot(C1),. . .**,dlnot(**Cm).

where k, n, m ≥ 0, and the Ai**s are all non-DL predicates (i.e. predicates that**
are not defined in the ontology), and the Bis and Ci**s are predicates that can**
be both defined in the rules and in the ontology. If k = n = m **= 0 then the** rule is a fact, and it is written as usual in Prolog, omitting the ':-' operator. Note that the transformation to include the negation N *Head* **in the body of** a rule for *Head* **as specified in Definition 3 is not needed: such a check is done** by the call to no prev neg/3 in known/3. To guarantee correctness, each rule must respect DL-safety. However, in the