Finally, we remark that the subset of flat MBNF theories in conjunctive normal form can be seen as a further extension of the framework of generalizal logic programming introduced by Inoue and Sakama (1994), which in turn is an extension of the disjunctive logic programming framework under the stable model semantics (Gelfond & Lifschitz, 1991).

Roughly speaking, flat MBNF theories in conjunctive normal form correspond to rules of generalized logic programs in which propositional formulas (instead of literals) are allowed as goals. The above computational characterization implies that such an extension of the framework of logic programming under the stable model semantics does not affect the worstcase complexity of the entailment problem, which is Π 2 -complete just like entailment in logic programs with disjunction under the stable model semantics (Eiter & Gottlob, 1995).  Such a result extends analogous properties (Marek, Truszczyński, & Rajasekar, 1995) to the case of disjunctive logic programs.

## 6. Conclusions

In this paper we have investigated the problem of reasoning in the propositional fragment of MBNF. The main results presented can be summarized as follows:

- the negation as failure modality not of MBNF exactly corresponds to negative introspection in AEL. This implies that the logic MBNF can be viewed as the conservative extension of two different nonmonotonic modal logics:  Halpern and Moses' logic of minimal knowledge S5 G and Moore's AEL;
- reasoning in the propositional fragment of MBNF lies at the third level of the polynomial hierarchy, hence (unless the polynomial hierarchy does not collapse) reasoning in MBNF is harder than reasoning in the best known propositional nonmonotonic logics, like default logic, autoepistemic logic, and circumscription;
- we have defined methods for reasoning in MBNF, which subsume and generalize wellknown nonmonotonic reasoning algorithms used in logic programming (Gelfond &
Lifschitz, 1991), default logic (Gottlob, 1992), and autoepistemic logic (Marek & Truszczyński, 1993);
- we have studied the flat fragment of MBNF and its relationship with the logic programming paradigm.
As for the computational aspects of reasoning in MBNF, the results presented in Section 5 prove that one source of complexity is due to the presence of nested occurrences of modalities in the theory, since reasoning in flat MBNF is computationally easier than in the general case.

It can be proven that another source of complexity lies in the underlying objective language. In fact, if we consider ' to be a tractable fragment of propositional logic, then the complexity of reasoning in the modal language 'M built upon ' is lower than in the general case. In particular, it is easy to see that, under the assumption that entailment can be computed in polynomial time, the algorithm MBNF-Not-Entails provides an in upper bound of Π for MBNF-entailment in the fragment M