Algor it hm  MBNF-Not-Entails(σ, ϕ)
Input: formula σ m, formula w B
Output: true if σ = mbnf ϕ , false otherwise.

begin if there exists partition (P, N) of M A(σ)
such that
(P, N) = Prt(Σ, ob(P, N)) and
(b) σ(P, N)
ϕ( ob ( P, N )) is satisfiable and
(c) for each partition (P ′ , N ′ ) = (P ′ N ′ ) of M A(σ),
(c1) σ(P ′ , N ′ ) is not satisfiable or (P', N') = Prt(E, ob(P', N'), ob(P, N)) or ob(P', N') is satisfiable
(c3) ob(P,N)
then return true else return false end Figure 1: Algorithm MBNF-Not-Entails.

## 4.2 Reasoning In Propositional Mbnf

We now define a deductive method for reasoning in general propositional MBNF theories.

Specifically, we present the algorithm MBNF-Not-Entails, reported in Figure 1, for computing entailment in MBNF.

The algorithm exploits the finite characterization of MBNF models given by Theorem 4.7 and an analogous finite characterization, in terms of partitions of M A(σ), of all the models relevant for establishing whether a partition ( P, N ) of M A( σ ) identifies an MBNF model.

The algorithm checks whether there exists a partition ( P, N ) of M A ( σ) satisfying the three conditions (a), (b), (c). Intuitively, the partition cannot be self-contradictory (condition (a)): in particular, the condition (P,N) = Prt(E, ob(P,N)) establishes that the objective knowledge implied by the partition ( P, N ) (that is, the formula ob( P, N )) identifies a set of interpretations M = I : I = ob(P,N) such that (M,M) induces the same partition (P, N) on MA(o). Moreover, the partition must be consistent with o and (condition (b)): such a condition implies that there exists an interpretation I such that both σ is satisfied in ( I, M, M ) and ϕ is not satisfied in the structure ( I, M, M ). Finally, condition (c) corresponds to check whether such a structure ( I, M, M ) identifies an MBNF
model for σ according to Definition 2.1, i.e. whether there is no pair ( J, M ′ ) such that M and (J, M', M) satisfies σ . Again, the search of such a structure is performed by M'
examining whether there exists a partition of M A ( σ ), different from ( P t N ), which does not stisfy any of the conditions (c1), (c2), (c3).

We illustrate the algorithm through the following simple example.

Example 4.13 Suppose σ = B (a B)
c