Input: A query **Query** to a DL-Atom Output: Value of the input query in *MKNF***W F S**
1 *addIndividuals(***Query***,IndividualList)*;
2 **foreach** Individual in *IndividualList* do 3 OutIter, *InIter* = 0; 4 S = S1 = {};
5 P = P1 = {};
6 **repeat**
7 P = P1; 8 **repeat**
9 S = S1; 10 **foreach** Class in *definedClass(Individual,Class)* do 11 Term = *Class(Individual)*;
12 S1 = S1∪ *known(Term, OutIter, InIter)*;
13 S1 = S1∪ *allModelsEntails(Term, OutIter, InIter)*;
14 S1 = S1∪ *allModelsEntails(neg(Term), OutIter, InIter)*;
15 end 16 **foreach** Role in definedRole(Individual,Individual1*,Role)* do 17 Term = *Role(Individual,Individual*1);
18 add Individual1 to *IndividualList* if necessary 19 S1 = S1∪ *known(Term, OutIter, InIter)*; 20 S1 = S1∪ *allModelsEntails(Term, OutIter, InIter)*; 21 S1 = S1∪ *allModelsEntails(neg(Term), OutIter, InIter)*;
22 end 23 *InIter*++;
24 **until** S = S1 ;
25 P = S;
26 *OutIter*++;
27 **until** *OutIter is even (a TU evaluation) and* P = P1 ;
28 end 29 if *known(***Query***,Outer***F inal** *-1,Inner* F inal) **then** 30 **return** true 31 **else**
32 if *known(***Query***,Outer***F inal** *,Inner'*F inal) **then**
33 **return** undefined 34 **else**
35 **return** false 36 end 37 end Fig. 2. The Top-Level Algorithm:*ComputeFixedPoint(Query)*

## 4.2.1 Rules Component

As mentioned, rules are transformed to use known/1 corresponding to K and dlnot/1 corresponding to not. As shown in Figure 3, given the goal known(A**) with**
A = p(O), the code first calls computeF ixedP oint(p(O**)) to perform the fixed point** computation for the object instance O. As in Figure 2, **computeF ixedP oint**(p(O))
calls the lower-level known/3 and dlnot/**3 to determine the truth of literals during**
the fixed point computation. Once the fixed point has been reached, known/1 uses