Query-driven Procedures for Hybrid MKNF Knowledge Bases · 11 Definition 2.13 Let K **be a ground Hybrid MKNF knowledge base. We define:**

$$\begin{array}{r}{\mathbf{N}_{0}=\mathsf{K}\mathsf{A}({\mathcal{K}})}\\ {\mathbf{N}_{n+1}=\Gamma_{{\mathcal{K}}}^{\prime}(\mathbf{P}_{n})}\\ {\mathbf{N}_{\omega}=\bigcap\mathbf{N}_{i}}\end{array}$$
$0\;=\;\psi$ . 
$$\mathbf{P}_{n+1}=\Gamma_{K}(\mathbf{N}_{n})$$ $$\mathbf{P}_{\omega}=\bigcup\mathbf{P}_{i}$$
P0 = ∅ N0 = KA(K)
Pn+1 = ΓK(Nn) Nn+1 = Γ′K(Pn)
Pω =[Pi Nω =\Ni
Pω contains everything that is necessarily true, while Nω **contains everything that**
is not false. Note that, by finiteness of the ground knowledge base, the iteration stops before reaching ω**. It was shown in [Knorr et al. 2011] that the sequences are** monotonically increasing, decreasing respectively. The two fixpoints can also be used to detect whether a knowledge base is MKNF-consistent or not [Knorr et al. 2011]. Theorem 2.14 Let K = (O,P) **be a ground Hybrid MKNF knowledge base.** K is MKNF-inconsistent iff Γ
′
K(Pω) ⊂ ΓK(Pω) or Γ
′
K(Nω) ⊂ ΓK(Nω) or O **is inconsistent.**
Intuitively, MKNF-consistency requires that O **is (first-order) consistent and that**
neither of the two additional conditions of Theorem 2.14 succeed.8 **These two**
comparisons ensure that the two fixpoints never contain contradictions and that there is no rule such that the truth value of the (conjunction in the) body is greater than the truth value of the head.

Example 2.15 **Consider the following KB** K1:
P(a) ← not P(a) Q(a) ← Q ⊑ ¬P
K1 is MKNF-inconsistent, since P(a**) is necessarily false, so the first rule violates**
the intuitive condition that the body should not have a higher truth value than the head. In fact, the computation yields that P(a**) is true and false at the same time,**
and the test reveals that. Consider the KB K2:

$\mathbb{Q}\subseteq\neg\mathbb{P}$? 
$$\mathbb{R}(\mathbf{a})$$
R ⊑ ¬P R(a)

$\mathbb{P}(\mathbf{a})\gets\mathbf{not}\,\mathbf{u}$ . 
P(a) ← not u u ← not u
P(a) is false, but u **is undefined, so that we obtain a rule with false head and** undefined body, and this is detected with the test.

If K **is MKNF-consistent, then the well-founded MKNF model exists.**
Definition 2.16 The well-founded MKNF model MW F **of an MKNF-consistent,**
ground Hybrid MKNF knowledge base K = (O,P**) is defined as**
MW F = {A | A ∈ Pω} ∪ {π(O)} ∪ {not B | B ∈ KA(K) \ Nω}.

8The formal definition of MKNF-consistency from [Knorr et al. **2011] would require the complete**
material on three-valued MKNF semantics, which we want to avoid.

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