Finally, the previous theorem provides a computational characterization of the logic of grounded knowledge and justified assumptions GK (Lin & Shoham, 1992). In fact, the logic GK can be considered as a syntactic variant of the propositional fragment of MKNF.

Therefore, skeptical entailment in GK is n 2 -complete. Remark. The computational properties of MBNF and its variants relate such formalisms to ground nonmonotonic modal logics (Eiter & Gottlob, 1992; Donini et al., 1997b; Rosati, 199).  Notably, ground nonmonotonic modal logics share with MBNF the interpretation in terms of minimal knowledge (or minimal belief) of the modality B ; specifically, as already mentioned, the propositional fragment of MBNF can be considered as built upon S5 G by adding a second modality not . Therefore, it turns out that, in the propositional case, adding a "negation by default" modality to the S5 logic of minimal knowledge does not increase the computational complexity of reasoning, while adding a minimal knowledge modality to AEL does increase the complexity of deduction. We can thus summarize as follows: minimal knowledge is computationally harder than negation as failure.

D
We now study the complexity of entailment for flat MBNF theories. First, it is known that, in the case of flat MBNF theories and subjective queries, entailment is Π 2 -complete:
membership in the class Π 2 is a consequence of the fact that flat MKNF theories can be polynomially embedded into McDermott and Doyle's nonmonotonic modal logic S4F
(Schwarz & Truszczyński, 1994, Proposition 3.2), whose entailment problem is Π t-complete
(Marek & Truszczyfiski, 1993), while Π 2 -hardness follows from the existence of a polynomialtime embedding of propositional default theories into flat MBNF theories (Lifschitz, 1994).

Therefore, the following property holds. Proposition 5.4 Let σ M and let φ σ = MBNF ϕ is Π 2 - complete.

B. Then, the problem of deciding whether As for complexity of entailment of generic queries with respect to flat MBNF theories, we analyze the complexity of the algorithm Flat-Not-Entails reported in Figure 2.  As shown before, both condition (a) and condition (b) can be checked through a linear number (with respect to the size of the input) of calls to an NP-oracle. Moreover, validity in modal logic S5 is a coNP-complete problem (Halpern & Moses, 1992). Hence, each of the conditions in the algorithm can be computed through a number of calls to an oracle for the propositional validity problem which is polynomial in the size of the input, and since the guess of the partition ( P t N ) of M A(σ) requires a nondeterministic choice, it follows that the algorithm runs in Σ 2 . Therefore, the following property holds.

M and let w Theorem 5.5  Let σ b.  Then, the problem of deciding whether σ =MBNF ϕ is Π 2 -complete.

Membership of the problem to the class Π 2 is implied by the algorithm Flat-not-
Proof.

entails, whereas n 2 -hardness is implied by Proposition 5.4.

D
Hence, the algorithm Flat-Not-Entails is "optimal" in the sense that it matches the lower bound for the entailment problem.