
## 10 · Jos´E J´Ulio Alferes Et Al.

The resulting KB is positive and we may apply TK **and obtain** {D(b), o(a), o(b)}.

Note that C(b) is not explicitly mentioned since it does not occur in KA(KG**). It is** nevertheless derivable from KG.

The MKNF transform resembles the well-known answer-set transformation [Gelfond and Lifschitz 1991] for logic programs. Based on it, an antitonic operator can be defined, but it is shown in [Knorr et al. 2011] that such an operator alone would not properly treat a problem called coherence**, i.e., classical negation would** not enforce default negation. Therefore, a second, slightly different transformation is introduced in [Knorr et al. 2011]. Definition 2.10 Let K = (O,P**) be a ground Hybrid MKNF knowledge base and** S ⊆ KA(K). The MKNF-coherent transform K//S is defined as K//S = (O,P//S),
where P//S contains all rules H ← A1, . . . , An **for which there exists a rule**
H ← A1, . . . , An, not B1, . . . , not Bm in P with Bj 6∈ S for all 1 ≤ j ≤ m and OBO,S 6|= ¬H. Example 2.11 Consider again K from Example 2.4 and let S be ∅. Then KG//S
is obtained:

| C ⊑ D       | C(b)        |
|-------------|-------------|
| C ⊓ E ⊑ ⊥   | p(a) ← o(a) |
| p(b) ← o(b) | o(a) ←      |
| E(a) ← o(a) | o(b) ←      |

The only rule that is removed is the one with head E(b), since C(b) holds and C and E are disjoint. Hence, OBO,∅ |= ¬E(b). We can apply TKG **to the resulting positive**
KB and obtain KA(KG) \ {E(b), D(a)}.

Note the difference between Definitions 2.8 and 2.10: we also remove a **rule from**
the MKNF-coherent transform, in case the classical negation of the head is derivable from the ontology augmented by S.

These two transformations can now be used to define two operators for Hybrid MKNF KBs as already hinted in the examples. Definition 2.12 Let K = (O,P**) be a ground Hybrid MKNF knowledge base and**
S ⊆ KA(K**). We define:**
ΓK(S) = lfp(TK/S) and Γ′K(S) = lfp(TK//S).

Both operators are shown to be antitonic [Knorr et al. 2011] and form the basis for defining the well-founded MKNF model. Here we present its alternating computation.

ACM Transactions on Computational Logic, Vol. V, No. N, September 2018.