
$$\varphi\quad=\quad$$
$$\begin{array}{c c c c}{{B\,b}}&{{\left(\begin{array}{c c c}{{}}&{{b}}&{{B\left(a}&{{}}&{{b}\right)}}\end{array}\right)}}\end{array}$$

Then, MA(σ) =  B(α    Bb), Bb, not(c
(Pl, Nl), where d), B   not b, not b . Now suppose that ( P, N ) =

$$P_{\mathrm{l}}$$
$=\quad\;B\left(a\quad\;B\,b\right),\,not\left(c\quad\quad d\,\right)$, $\,not\,\,b\,\,\,c$  $=\quad\;B\,b,\,B\quad\,not\,\,b$  . 
Then, σ(P, N) = true   (true   false)   c (which is equivalent to c), and ob(P, N) = a    false
(which is equivalent to a). Now, let M =  I : I = a : it is easy to see that ( M, M )
sset to the modal atoms in P, while it does not satisfy the modal atoms in N, hence (P, N) =  Prt(E, ob(P, N)), thus satisfying condition (a) of the algorithm.  Then, since a   b is not a valid propositional formula, M = B(a   b), hence   ϕ(ob(P,N)) =
a
(true (  b   false)), which is equivalent to false. Therefore, σ(P, N)
ϕ(ob(P, N)) is not satisfiable, thus condition (b) does not hold.

Suppose now that (P, N) = (P, N,), where

$P_{2}=B(a\quad B\,b),\,not\,(c\quad\;d\,),\,Bb,\,B\quad not\;\;b\;)$  $N_{2}=\quad not\;\;b$  . 
Then, σ(P, N) = true   (true true)  c (which is equivalent to c), and ob(P, N) = (α true) b true, which is equivalent to b. Again, it is easy to see that ( P, N ) = Prt( Σ, ob( P, N )), thus stisfying condition (a) of the algorithm. Then, since b a ab is not a valid propositional formula,   ϕ( ob ( P, N )) =    (false   (  b   false)), which is equivalent to true.  Hence, σ( P, N )
ϕ( ob ( P t N )) is equivalent to c , which implies that condition ( b ) holds. Finally, it is easy to verify that either condition (c1) or condition (c2) holds for each partition of MA(σ)
different from ( P 2 , N 2 ), with the exception of ( P 1 , N 1 ).  So let ( P ′ , N ′ ) = ( P 1 , N 1 ):  as shown before, ob(P', N') is equivalent to a, hence ob(P, N) is ob(P', N') is equivalent to b therefore condition (c3) holds for ( P ′ , N ′ ) = ( P 1 , N 1 ), which implies that condition (c)
holds for ( P, N ) = ( P, N 2 ). Consequently, MBNF-Not-Entails( σ, ϕ) returns true. In fact, the partition ( P 2 , N 2 ) identifies the set of MBNF models for σ ( I , M ) such that I is an interpretation satisfying c and M = I : I = b . Each su model does not satisfy the query ϕ : indeed, it can immediately be verified that, for each interpretation I , ( I , M , M ) =
Bb ( b  B(a  b)), since M = B(a  b) and M = Bb.

D
To prove correctness of the algorithm MBNF-Not-Entails we need the following preliminary lemma.

Lemma 4.14 Let σ Let M " = I : I = ob(P,N) . Then, (P,N) is the partition induced by (M", M).

The proof is by induction on the depth of the modal atoms of MA(Σ).  Let Proof.

M M A ( Σ ) such that ψ     : then, ( M ′ , M ) = not ψ iff there exists an interpretation not ψ M such that I = ψ, therefore ( M ′, M ) = not ψ iff ( M ′′, M ) = not ψ. Now let Bψ I
M 