characterization of reasoning in MBNF.  We conclude in Section 6.  This paper is an extended and thoroughly revised version of (Rosati, 1997).

## 2. The Logic Mbnf

In this section we briefly recall the logic MBNF (Lifschitz, 1994), which is a modal logic with two epistemic operators: a "minimal belief" modality B and a "negation as failure" (also called "negation by default") modality not. We use We use We use to denote a fixed propositional language built in the usual way from: (i) an alphabet of propositional symbols; (ii) the symbols true, false; (iii) the propositional connectives modal extension of   with the modalities B and not. We say that a formula ϕ M
has (modal) depth i (with i 0) if each subformula in ϕ lies within the scope of at most i modalities, and there exists a subformula in φ which lies within the scope of exactly i modalities.

We denote as ~, the set of subjective MBNF formulas, i.e. the subset of formulas from m in whi ea occurrence of a propositional symbol lies within the scope of at least one modality, and with         the set of flat MBNF formulas, that is the set of formulas from in whi ea propositional symbol lies within the scope of exactly one modality. We call a modal formula ϕ from B denotes the set of positive formulas from occur in w.

positive formulas from We now recall the notion of MBNF model. An interpretation is a set of propositional symbols.  An MBNF  structure is a triple ( I , M b , M n ), where I is an interpretation (also called initial world) and Mb, Mn are non-empty sets of interpretations (worlds). Satisfiability of a formula in an MBNF structure is defined inductively as follows:
1. if ϕ is a propositional symbol, ϕ is satisfied by (I, M,, M,) iff ϕ   I;

2. ϕ is satisfied by ( I, M b, M n ) iff ϕ is not satisfied by ( I, M b, M n );
3. ϕ 1 ϕ 2 is satisfied by ( I , M b , M n ) iff ϕ 1 is satisfied by ( I , M b , M n ) and ϕ 2 is satisfied by (I, M,, M,);
ϕ 2 is satisfied by ( I , M b , M n ) iff either ϕ 1 is satisfied by ( I , M b , M n ) or ϕ 2 is 4. vi satisfied by (I, M, M,);
5. ϕ 1   ϕ 2 is satisfied by ( I , M b , M n ) iff either ϕ 1 is not satisfied by ( I , M b , M n ) or ϕ 2 is satisfied by (I, M, M,);
6. B ϕ is satisfied by ( I , M b , M n ) iff, for every J    M b , ϕ is satisfied by ( J, M b , M n );
7. not ϕ is satisfied by ( I, M b, M n ) iff there exists J M n such that ϕ is not satisfied by
(J, M,, M,,).
We write (I, M,, M,) = ϕ to indicate that ϕ is satisfied by (I, M,, M,). We say that a theory  Σ
M is satisfied by (I, M,, M,) (and write (I, M,, M,) = Σ) iff each formula from E is satisfied by (I, M,, M,). If Q
the initial interpretation I : thus, in this case we also write ( M b, M n ) = Q . Analogously, if