known (A):-
computeFixedPoint (A) ,
get_object_iter (A , OutIter , InIter ) , known (A , OutIter , InIter ).

:- table known /3.

known (A , OutIter , InIter ):-
PrevIter is InIter - 1,
( call (A) ,
;
InIter > 0, allModelsEntails (A , OutIter , PrevIter )
) ,
( OutIter mod 2 =:= 1 ->
true
;
no_prev_neg (A , OutIter , PrevIter )
).

/* Enforce coherence of default negation with first - order negation */
no_prev_neg (_A , _OutIter , PrevIter ) :-
PrevIter < 0 ,!.

no_prev_neg (A , OutIter , PrevIter ) :-
tnot ( allModelsEntails ( neg (A) , OutIter , PrevIter )).

Fig. 3. Prolog Implementation of K **for Class Properties**
dlnot (A):-
computeFixedPoint (A) , get_object_iter (A , OutIter , _InIter ) ,
dlnot (A , OutIter ).

/* In first iteration , ensure that TU = KA (K *) */
dlnot (_A ,0) :- !.

/* In subsequent iterations , check previous outer iteration */
dlnot (A , OutIter ):-
PrevIter is OutIter - 1, get_final_iter (A , PrevIter , FinIter ) ,
tnot ( known (A , PrevIter , FinIter )).

Fig. 4. Prolog Implementation of not **for Class Properties**
may be added to the fixed point set of individuals. As is usual with tableau provers, entailment of a formula ϕ by an ontology O **is shown if the classical negation of** ϕ is inconsistent with O**. Thus,** rec *alModelsEntails/2* **immediately fails if the classical** negation of ϕ is consistent with O in the present iteration; otherwise, ϕ is entailed.