get object *iter(p(O),Outer,Inner)* to obtain the final iteration indices for O **from a** global store, and calls known/**3 again to determine the final truth value of** p(O).

Note that known/**3 is always called with the iteration indices (arguments 2 and**
3) bound, so that they are always contained in the table entries. Thus, the postfixed point call to known/**3 simply checks the table, and is not computationally**
expensive.

Within a given iteration, p(O**) may be known in one of two ways. Either it can**
be directly derived from the rules; or O ∈ P **(i.e.** o:P**) may have been entailed** by the ontology in the previous inner iteration step, as determined by the call allModelsEntails(p(O), OutIter, P revIter**). In either case, care must be taken so**
that that if ¬A holds, then not A **holds as well. In the formalism of Definition 3 this**
is guaranteed in two steps. First, an axiom ¬P ⊑ NP **is added for each DL-atom**
that occurs in the head of a rule; in addition, the literal not NP **is added the body**
of each rule with head P: this rewrite is used by the Γ′K **operator to produce the**
T U set. Accordingly in Figure 3, when we try to derive known(**A, OutIter, InIter**)
and OutIter is even (i.e. corresponding to a T U step via Γ′K **in Definition 7 ) we**
check whether the ontology derived ¬A **in the previous inner iteration by the call**
no prev neg(A, OutIter, P revIter). If ¬A was derived, then no prev neg/**3 fails via** the call to tnot/**1, (which is XSB's operator for tabled negation), and the top-level**
goal also fails.

On the other hand, the predicate dlnot(A**) which uses closed world assumption,**
succeeds if A fails (Figure 4). As discussed in Example 5, the evaluation of **dlnot/**2 must take into account the result of the previous *outer* **iteration. Accordingly, in** Figure 4 the call dlnot(A) with A = p(O**) gets the current outer iteration for** O, and immediately calls dlnot/**2. If the outer iteration index is greater than 1, the** second clause of dlnot/**2 simply finds the index of the (inner) fixed point of the**
previous outer iteration, and determines whether A **was true in that fixed point.**
Since the call to known/3 in tnot/**1 is tabled,** *dlnot/[1,2]* **do not need to be tabled** themselves. As described before, outer iterations alternately represent iterations of T and T U sets of Definition 7, where T sets are monotonically increasing while T U sets are monotonically decreasing. To assure that the first T U **set is the largest set**
(KA(K∗) following Definition 6), we compel all calls to dlnot/**1 to succeed in the**
first outer iteration, as represented by the first clause of **dlnot/**2.

## 4.2.2 Ontology Component

The tabled predicate *allModelsEntails/3* **provides the interface to CDF's tableau** theorem prover (Figure 5). It is called with an atom or its classical negation, and with the its iteration indices bound. Although the iterations are not used in the body of *allModelsEntails/3***, representing the iteration information in the head ensures** its availability in table entries for use by known/3. *allModelsEntails/3* **first converts** the atomic form of a proposition to one used by CDF. That is, it translates a 1ary DL-atom representing an individual's class membership to the CDF **predicate**
isa/**2, and a 2-ary DL-atom representing an individual's role to the CDF predicate**
hasAttr/3 (see Section 3). In addition, if Atom is a 2-ary role, the target individual