ψ(P, N) such that Bψ   P. Therefore, P ′ = P, which implies that (P ′ , N ′ ) = (P, N).

Then, since ( J, M ′ , M ) = σ , by Lemma 4.6 J = σ ( P ′ , N ′ ), hence σ ( P ′ , N ′ ) is satisfiable. Now let M n = I : I = ob(P l , N l ) . By Lemma 4.14, it follows that (P l , N l ) is the partition induced by ( M ′′ , M ), therefore, by Definition 4.8, ( P ′ , N ′ ) = Prt( Σ, ob( P ′ , N ′ ), ob( P, N ′ )).

Moreover, since M'   M, it follows that the propositional formula ob(P, N)   ob(P', N') wis valid, hence the formula ob ( P, N )
ob(P ′ , N ′ ) is unsatisfiable. Consequently, (P ′ , N ′ )
does not satisfy condition (c) in the algorithm, thus contradicting the hypothesis. Therefore, (I, M) is an MBNF model for σ, and since (I, M, M) = ϕ, it follows that σ = MBNF ϕ, thus proving the thesis.

D
We point out the fact that the algorithm MBNF-Not-Entails does not rely on a theorem prover for a modal logic: thus, "modal reasoning" is not actually needed for reasoning in MBNF. This is an interesting peculiarity that MBNF shares with other nonmonotonic modal formalisms, like autoepistemic logic (Moore, 1985) or the autoepistemic logic of knowledge (Schwarz, 1991).

## 4.3 Reasoning In Flat Mbnf

We now study reasoning in flat MBNF theories.  The main reason for taking into account the flat fragment of MBNF is the fact that reasoning in many of the best known nonmonotonic formalisms like default logic, circumscription, and logic programming, can be reduced to reasoning in flat MBNF theories (Lifschitz, 1994).

It is known that, if σ M and w g, then it is possible to reduce the entailment σ =MBNF ϕ to reasoning in logic S4F MDD ; by translating MBNF formulas into unimodal formulas of S4F MDD (Schwarz & Truszczyiiski, 1994). Thus, the procedure for deciding entailment in the logic S4F MDD presented by Marek and Truszczynski (1993) can be employed for computing the entailment σ = mbnf ϕ . In the following we study a more general problem, that is entailment σ = mbnf ϕ in the case σ M and w b, and present a specialized algorithm for this problem, whi is simpler than the more general reasoning method for S4F MDD ·
In Figure 2 we report the algorithm Flat-Not-Entails for computing such an entailment.

In the algorithm, Pn denotes the subset of modal atoms from P prefixed by the modality not, i.e. Pn =  not ψ : not ψ P
Informally, correctness of the algorithm Flat-Not-Entails is established by the fact that,
,, then (a), (b), and (c) are necessary and sufficient conditions on a partition ( P, N )
if σ in order to establish whether it is induced by a pair ( M, M) such that there exists an MBNF model for σ of the form ( I, M ). In particular, condition (c) states that B ( ob ( P, N )) must be a consequence of σ( P n , N ) in modal logic S5, 1 since it can be shown that if σ( P n , N )
B(ob(P,N)) is not valid in S5, then the guess on the modal atoms of the form Bϕ in P is not minimal. We illustrate this fact through the following example.

## Example 4.16 Let

not (c d)) (B(a b) Bc) Bc