Reasoning about Minimal Belief and Negation as Failure

Riccardo Rosati
Dipartimento di Informatica e Sistemistica
Università di Roma ``La Sapienza''
Via Salaria 113, 00198 Roma, Italy
email: rosati@dis.uniroma1.it

Abstract:

We investigate the problem of reasoning in the propositional fragment of ${\rm MBNF}$ , the logic of minimal belief and negation as failure introduced by Lifschitz, which can be considered as a unifying framework for several nonmonotonic formalisms, including default logic, autoepistemic logic, circumscription, epistemic queries, and logic programming. We characterize the complexity and provide algorithms for reasoning in propositional ${\rm MBNF}$ . In particular, we show that skeptical entailment in propositional ${\rm MBNF}$ is $\Pi^p_3$ -complete, hence it is harder than reasoning in all the above mentioned propositional formalisms for nonmonotonic reasoning. We also prove the exact correspondence between negation as failure in ${\rm MBNF}$ and negative introspection in Moore's autoepistemic logic.

Introduction

Research in the formalization of commonsense reasoning has pointed out the need of formalizing agents able to reason introspectively about their own knowledge and ignorance [27,20]. Modal epistemic logics have thus been proposed, in which modalities are interpreted in terms of knowledge or belief. Generally speaking, the conclusions an introspective agent is able to draw depend on both what she knows and what she does not know. Hence, any such conclusion may be retracted when new facts are added to the agent's knowledge. For this reason, many nonmonotonic modal formalisms have been proposed in order to characterize the reasoning abilities of an introspective agent.

Among the nonmonotonic modal logics proposed in the literature, the logic of minimal belief and negation as failure ${\rm MBNF}$ [21,22] is one of the most studied formalisms [3,2,1]. Roughly speaking, such a logic is built by adding to first-order logic two distinct modalities, a ``minimal belief'' modality B and a ``negation as failure'' modality ${\it not}$ . The logic thus obtained is characterized in terms of a nice model-theoretic semantics. ${\rm MBNF}$ has been used in order to give a declarative semantics to very general classes of logic programs [23,36,16], which generalize the stable model semantics of negation as failure in logic programming [9,10,11]. Also, ${\rm MBNF}$ can be viewed as an extension of the theory of epistemic queries to databases [30], which deals with the problem of querying a first-order database about its own knowledge. Due to its ability of expressing many features of nonmonotonic logics [22,36], ${\rm MBNF}$ is generally considered as a unifying framework for several nonmonotonic formalisms, including default logic, autoepistemic logic, circumscription, epistemic queries, and logic programming.

Although several aspects of the logic ${\rm MBNF}$ have been thoroughly investigated [36,3,2], the existing studies concerning the computational properties of ${\rm MBNF}$ are limited to subclasses of propositional ${\rm MBNF}$ theories [16] or to a very restricted subset of the first-order case [1].

In this paper we present a computational characterization of deduction in the propositional fragment of ${\rm MBNF}$ . In particular, we show that logical implication in the propositional fragment of ${\rm MBNF}$ is a $\Pi^p_3$ -complete problem: hence, it is harder (unless the polynomial hierarchy collapses) than reasoning in all the best known propositional formalisms for nonmonotonic reasoning, like autoepistemic logic [28,12], default logic [12], circumscription [7], (disjunctive) logic programming [8], and several McDermott and Doyle's logics [25]. As shown in the following, this result also implies that minimal knowledge is computationally harder than negation as failure.

Moreover, we study the subclass of flat ${\rm MBNF}$ theories, i.e. ${\rm MBNF}$ theories without nested occurrences of modalities, showing that in this case logical implication is $\Pi^p_2$ -complete. This case is the most interesting one from the logic programming viewpoint. Indeed, it implies that, under the stable model semantics, increasing the syntax of program rules, by allowing propositional formulas as goals in the rules, does not affect the worst-case complexity of query answering for disjunctive logic programs with negation as failure.

Furthermore, we provide algorithms for reasoning both in ${\rm MBNF}$ and in its flat fragment, which are optimal with respect to worst-case complexity. Notably, such deductive methods can be considered as generalizations of known methods for reasoning in nonmonotonic formalisms such as default logic, autoepistemic logic, and logic programming under stable model semantics.

We also show that the ``negation as failure'' modality in ${\rm MBNF}$ exactly corresponds to negative introspection in autoepistemic logic [27]. This result implies that the logic ${\rm MBNF}$ can be considered as the ``composition'' of two epistemic modalities: the ``minimal knowledge'' operator due to [14] and Moore's autoepistemic operator.

Besides its theoretical interest, we believe that such a computational and epistemological analysis of ${\rm MBNF}$ has interesting implications for the development of knowledge representation systems with nonmonotonic abilities, since it allows for a better understanding and comparison of the different nonmonotonic formalisms captured by ${\rm MBNF}$ . The interest in defining deductive methods for ${\rm MBNF}$ also arises from the fact that such a logic, originally developed as a framework for the comparison of different logical approaches to nonmonotonic reasoning, has recently been considered as an attractive knowledge representation formalism. In particular, it has been shown [4] that the full power of ${\rm MBNF}$ is necessary in order to logically formalize several features of implemented frame-based knowledge representation systems.

In the following, we first briefly recall the logic ${\rm MBNF}$ . In Section 3 we address the relationship between ${\rm MBNF}$ and Moore's autoepistemic logic. Then, in Section 4 we study the problem of reasoning in propositional ${\rm MBNF}$ : we first consider the case of general ${\rm MBNF}$ theories, then we deal with flat ${\rm MBNF}$ theories. In Section 5 we present the computational characterization of reasoning in ${\rm MBNF}$ . We conclude in Section 6. This paper is an extended and thoroughly revised version of [31].

The Logic MBNF

In this section we briefly recall the logic ${\rm MBNF}$ [22], 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 ${\it not}$ . We use ${\cal L}$ to denote a fixed propositional language built in the usual way from: (i) an alphabet ${\cal A}$ of propositional symbols; (ii) the symbols $\mbox{{\it true}}$ , $\mbox{{\it false}}$ ; (iii) the propositional connectives $\vee,\wedge,\neg,\supset$ . We denote as ${\cal L}_M$ the modal extension of ${\cal L}$ with the modalities B and ${\it not}$ . We say that a formula $\varphi \in{\cal L}_M$ has (modal) depth i (with $i\geq 0$ ) if each subformula in $\varphi$ lies within the scope of at most i modalities, and there exists a subformula in $\varphi$ which lies within the scope of exactly i modalities.

We denote as ${\cal L}_M^S$ the set of subjective ${\rm MBNF}$ formulas, i.e. the subset of formulas from ${\cal L}_M$ in which each occurrence of a propositional symbol lies within the scope of at least one modality, and with ${\cal L}_M^1$ the set of flat ${\rm MBNF}$ formulas, that is the set of formulas from ${\cal L}_M$ in which each propositional symbol lies within the scope of exactly one modality. We call a modal formula $\varphi$ from ${\cal L}_M$ positive (resp. negative) if the modality ${\it not}$ (resp. B) does not occur in $\varphi$ . ${\cal L}_B$ denotes the set of positive formulas from ${\cal L}_M$ , while ${\cal L}_B^S$ denotes the set of positive formulas from ${\cal L}_M^S$ .

We now recall the notion of ${\rm MBNF}$ model. An interpretation is a set of propositional symbols. An ${\rm MBNF}$ structure is a triple (I,M_b,M_n), where I is an interpretation (also called initial world) and M_b,M_n are non-empty sets of interpretations (worlds). Satisfiability of a formula in an ${\rm MBNF}$ structure is defined inductively as follows:

We write $(I,M_b,M_n)\models \varphi$ to indicate that $\varphi$ is satisfied by (I,M_b,M_n). We say that a theory $\Sigma\subseteq{\cal L}_M$ is satisfied by (I,M_b,M_n) (and write $(I,M_b,M_n)\models\Sigma$ ) iff each formula from $\Sigma$ is satisfied by (I,M_b,M_n). If $\varphi\in{\cal L}_M^S$ , then the evaluation of $\varphi$ is insensitive to the initial interpretation I: thus, in this case we also write $(M_b,M_n)\models\varphi$ . Analogously, if $\varphi\in{\cal L}_B^S$ , then the evaluation of $\varphi$ is insensitive both to the initial interpretation I and to the set M_n, and we also write $M_b\models\varphi$ . If $\varphi\in{\cal L}$ then the evaluation of $\varphi$ does not depend on the sets M_b,M_n, and in this case we write $I\models\varphi$ .

In order to relate ${\rm MBNF}$ structures to standard interpretation structures in modal logic (i.e. Kripke structures), we remark that, due to the above notion of satisfiability, we can consider the sets M_b, M_n in an ${\rm MBNF}$ interpretation structure as two distinct universal Kripke structures, i.e. possible-world structures in which each world is connected to all worlds of the structure. In fact, since the accessibility relation in such a structure is universal, without loss of generality it is possible to identify a universal Kripke structure with the set of interpretations contained in it. We recall that the class of universal Kripke structures characterizes the logic ${\bf\sf S5}$ [25, Theorem 7.52].

The nonmonotonic character of ${\rm MBNF}$ is obtained by imposing the following preference semantics over the interpretation structures satisfying a given theory.

We say that a formula $\varphi$ is entailed (or logically implied) by $\Sigma$ in ${\rm MBNF}$ (and write $\Sigma\models_{{\rm MBNF}}\varphi$ ) iff $\varphi$ is satisfied by every ${\rm MBNF}$ model of $\Sigma$ . In order to simplify notation, we denote the ${\rm MBNF}$ model (I,M,M) with the pair (I,M), and, if $\Sigma\in{\cal L}_M^S$ , we denote (I,M,M) with M, since in this case the evaluation of $\Sigma$ is insensitive to the initial world I, namely, if (I,M) is a model for $\Sigma$ , then, for each interpretation J, (J,M) is a model for $\Sigma$ .

Example 2.3 Let $\Sigma= \{{\it not}\: {\it married}\supset B\:{\it hasNoChildren}\}$ . It is easy to see that the only models for $\Sigma$ are of the form (I,M) such that $M=\{I:I\models {\it hasNoChildren}\}$ , since ${\it married}$ can be assumed not to hold by the agent modeled by $\Sigma$ , which is then able to conclude $B\:{\it hasNoChildren}$ . Notably, the meaning of $\Sigma$ is analogous to the default rule $\frac{:\neg {\it married}}{{\it hasNoChildren}}$ in Reiter's default logic [22]. Also, let $\Sigma=\{\k\,{\it bird}\wedge{\it not}\neg\,{\it flies}\supset \k\,{\it flies}, \k\,{\it bird}\}$ . In a way analogous to the previous case, it can be shown that the only MBNF models for $\Sigma$ are of the form (I,M), with $M=\{I:I\models {\it bird}\wedge{\it flies}\}$ . Therefore, $\Sigma\models_{\rm MBNF}\k\,{\it flies}$ . As shown by [22], $\Sigma$ corresponds to the default theory $(\{\frac{{\it bird}:{\it flies}}{{\it flies}}\},{\it bird})$ .

Given a set of interpretations M, Th(M) denotes the set of formulas $B\varphi$ such that $B\varphi\in{\cal L}_B$ and $M\models B\varphi$ . Let M₁,M₂ be sets of interpretations. We say that M₁ is equivalent to M₂ iff Th(M₁)=Th(M₂).

It turns out that, when restricting to theories composed of subjective positive formulas, MBNF corresponds to the modal logic of minimal knowledge due to [14], also known as ground nonmonotonic modal logic ${\bf\sf S5}_G$ [19,5]. In fact, ${\bf\sf S5}_G$ is obtained from modal logic ${\bf\sf S5}$ by imposing the following preference order over the universal Kripke structures satisfying a theory $\Sigma\in{\cal L}_B$ : M is a model for $\Sigma$ iff $M\models\Sigma$ and, for each M', if $M'\models\Sigma$ then $M'\not\supset M$ [38]. In fact, it is immediate to see that the ${\rm MBNF}$ semantics of theories composed of subjective positive formulas corresponds to the above semantics according to ${\bf\sf S5}_G$ . Hence, the following property holds.

The previous proposition implies that, when $\Sigma\subseteq{\cal L}_B^S$ , a set of interpretations M satisfying $\Sigma$ is compared with all other sets of interpretations satisfying $\Sigma$ , while, in the case $\Sigma\subseteq{\cal L}_M$ , M is only compared with the sets M' such that (M',M) satisfies $\Sigma$ .

Hence, the main difference between MBNF and ${\bf\sf S5}_G$ lies in the fact that in ${\bf\sf S5}_G$ all models are maximal with respect to set containment (or minimal with respect to the objective knowledge which holds in the model), while in MBNF this property is not generally true. E.g., the theory $\Sigma=\{{\it not}\:{\it married}\vee B\:{\it married}\}$ has two types of models, for each possible choice of the initial world J: (J,M₁), where M₁ corresponds to the set of all interpretations (which represents the case in which ${\it married}$ is not assumed to hold); and (J,M₂), where $M_2=\{I:I\models {\it married}\}$ . Namely, if ${\it married}$ is assumed to hold, then $\Sigma$ forces one to conclude $B\:{\it married}$ : that is, the initial assumption is justified by the knowledge derived on the basis of such an assumption [24]. We remark that, by Proposition 2.5, the interpretation of the ${\rm MBNF}$ operator B exactly corresponds to the interpretation of the modality B in ${\bf\sf S5}_G$ .

Relating MBNF to Autoepistemic Logic

In this section we study the relationship between autoepistemic logic and ${\rm MBNF}$ . First, we briefly recall Moore's autoepistemic logic ( ${\rm AEL}$ ). In order to keep notation to a minimum, we change the language of ${\rm AEL}$ , using the modality B instead of L. Thus, in the following a formula of ${\rm AEL}$ is a formula from ${\cal L}_B$ .

Given a theory $\Sigma\subseteq{\cal L}_B$ and a formula $\varphi\in{\cal L}_B$ , we write $\Sigma\models_{\rm AEL}\varphi$ iff $\varphi$ belongs to all the stable expansions of $\Sigma$ . Each stable expansion T is a stable set according to the following definition [39].

We recall that a stable set T corresponds to a maximal universal Kripke structure M_T such that T is the set of formulas satisfied by M_T [25]. With the term ${\rm AEL}$ model for $\Sigma$ we will thus refer to a set of interpretations M whose set of theorems Th(M) corresponds to a stable expansion for $\Sigma$ in ${\rm AEL}$ .

Finally, notice that we have adopted the notion of consistent autoepistemic logic [25], i.e. in (1) we do not allow the inconsistent theory $T={\cal L}_B$ composed of all modal formulas to be a (possible) stable expansion. The results presented in this section can be easily extended to this case (corresponding to Moore's original proposal): however, this requires to slightly change the semantics of ${\rm MBNF}$ , allowing in Definition 2.1 the empty set of interpretations to be a possible component of ${\rm MBNF}$ structures.

In the following, we use the term embedding (or translation) to indicate a transformation function $\tau(\cdot)$ for modal theories. We are interested in finding a faithful embedding [13,35,17], in the following sense: $\tau(\cdot)$ is a faithful embedding of ${\rm AEL}$ into ${\rm MBNF}$ if, for each theory $\Sigma\subseteq{\cal L}_B$ and for each model M, M is an ${\rm AEL}$ model for $\Sigma$ iff M is an ${\rm MBNF}$ model for $\tau(\Sigma)$ .

It is already known that ${\rm AEL}$ theories can be embedded into ${\rm MBNF}$ theories. In particular, it has been proven [24,37] that ${\rm AEL}$ theories with no nested occurrences of B (called flat theories) can be embedded into ${\rm MBNF}$ ; now, since in ${\rm AEL}$ any theory can be transformed into an equivalent flat theory (which has in general size exponential in the size of the initial theory), it follows that any ${\rm AEL}$ theory can be embedded into ${\rm MBNF}$ .

However, we now prove a much stronger result: negation as failure in ${\rm MBNF}$ exactly corresponds to negative introspection in ${\rm AEL}$ , i.e. ${\rm AEL}$ 's modality $\neg B$ and ${\rm MBNF}$ 's modality ${\it not}$ are semantically equivalent. Hence, such a correspondence is not only limited to modal theories without nested modalities, and induces a polynomial-time embedding of any ${\rm AEL}$ theory into ${\rm MBNF}$ .

We first define the translation $\tau(\cdot)$ of modal theories from ${\rm AEL}$ to ${\rm MBNF}$ theories.

We now show that the translation $\tau(\cdot)$ embeds ${\rm AEL}$ theories into ${\rm MBNF}$ . To this aim, we exploit the semantic characterization of ${\rm AEL}$ defined by [34]. Roughly speaking, according to such a preference semantics over possible-world structures, an ${\rm AEL}$ model for $\Sigma$ is a set of interpretations M satisfying $\Sigma$ such that, for any interpretation J not contained in M, the pair (J,M) does not satisfy $\Sigma$ . Formally:

In the following, we say that an occurrence of a subformula $\psi$ in a formula $\varphi \in{\cal L}_M$ is strict if it does not lie within the scope of a modal operator. E.g., let $\sigma= B\varphi \wedge {\it not}(B\psi\vee\xi)$ . The occurrence of $B\varphi$ in $\sigma$ is strict, while the occurrence of $B\psi$ is not strict.

Proof. If part. Suppose (I,M) is an ${\rm MBNF}$ model of $\tau(\Sigma)$ . Then, for each $M'\supset M$ , $(M',M)\not\models\tau(\Sigma)$ . Since $\tau(\Sigma)$ is a set of formulas of the form $B\varphi$ , where $\varphi$ does not contain any occurrence of the operator B, it follows that, for each subformula of the form ${\it not}\:\varphi$ occurring in $\tau(\Sigma)$ , $(M',M)\models{\it not}\:\varphi$ iff $(M,M)\models{\it not}\:\varphi$ . Now let $B\varphi \in\tau(\Sigma)$ , let $\varphi '$ denote the propositional formula obtained from $\varphi$ by replacing each strict occurrence in $\varphi$ of a formula of the form ${\it not}\:\psi$ with $\mbox{{\it true}}$ if $(M,M)\models{\it not}\:\psi$ and with $\mbox{{\it false}}$ otherwise, and let $\Sigma'=\{\varphi ' : B\varphi \in\tau(\Sigma)\}$ . Now suppose there exists an interpretation J such that $J\models\Sigma'$ and $J\not\in M$ . Then, from the definition of satisfiability in ${\rm MBNF}$ structures it follows that $(M\cup\{J\},M)\models\tau(\Sigma)$ , thus contradicting the hypothesis that (I,M) is an MBNF model for $\tau(\Sigma)$ . Hence, $M=\{I:I\models\Sigma'\}$ . Now consider a pair (J,M): again, from the definition of satisfiability in ${\rm MBNF}$ structures it follows immediately that $(J,M) \models\Sigma$ iff $J\models\Sigma'$ . And since M contains all the interpretations satisfying $\Sigma'$ , it follows that, for each interpretation $J\not\in M$ , $(J,M)\not\models\Sigma$ , therefore by Proposition 3.4 it follows that M is an ${\rm AEL}$ model for $\Sigma$ .

Only-if part. Suppose M is an ${\rm AEL}$ model for $\Sigma$ . Then, by Proposition 3.4, for each interpretation $I\in M$ , $(I,M)\models \Sigma$ and, for each interpretation $J\not\in M$ , $(J,M)\not\models\Sigma$ . For each $\varphi \in\Sigma$ , let $\varphi ''$ denote the propositional formula obtained from $\varphi$ by replacing each strict occurrence of a formula of the form $B\psi$ with $\mbox{{\it true}}$ if $M\models B\psi$ and with $\mbox{{\it false}}$ otherwise, and let $\Sigma''=\{\varphi '' : \varphi \in\Sigma\}$ . Then, suppose there exists an interpretation J such that $J\models\Sigma''$ and $J\not\in M$ . Then, from the definition of satisfiability in ${\rm MBNF}$ structures it follows that $(J,M) \models\Sigma$ , thus contradicting the hypothesis that M is an AEL model for $\Sigma$ . Hence, $M=\{I:I\models\Sigma''\}$ . Now suppose that, for some interpretation I, (I,M) is not an MBNF model for $\tau(\Sigma)$ . Then, there exists $M'\supset M$ such that $(M',M)\models\tau(\Sigma)$ . From the definition of $\tau(\cdot)$ , it follows that each interpretation in M' satisfies $\Sigma''$ , and, since $M'\supset M$ , there exists $J\not\in M$ such that $J\models\Sigma''$ . Contradiction. Therefore, (I,M) is an MBNF model for $\Sigma$ . $\Box$

We remark that the above theorem could alternatively be proved from the fact that the K-free fragment of the logic ${\rm MKNF}$ [21] is equivalent to ${\rm AEL}$ , which is stated (although without proof) by [37, page 123], and from the correspondence between ${\rm MBNF}$ and ${\rm MKNF}$ [22].

The previous theorem implies that the interpretation of the modality ${\it not}$ in ${\rm MBNF}$ and of the modal operator in autoepistemic logic are the same. This property extends previous results relating ${\rm MBNF}$ with ${\rm AEL}$ [24,36,3], and has interesting consequences both in the logic programming framework and in nonmonotonic reasoning. In particular, since ${\rm MBNF}$ generalizes the stable model semantics for logic programs [9], the above result strengthens the idea that ${\rm AEL}$ is the true logic of negation as failure (as interpreted according to the stable model semantics). Moreover, positive theories have the same interpretation both in ${\rm MBNF}$ and in the logic of minimal knowledge ${\bf\sf S5}_G$ [14]: consequently, the logic ${\rm MBNF}$ generalizes both Halpern and Moses' ${\bf\sf S5}_G$ and Moore's ${\rm AEL}$ .

Reasoning in MBNF

In this section we present algorithms for reasoning in propositional ${\rm MBNF}$ : in particular, we study the entailment problem in ${\rm MBNF}$ . From now on, we assume to deal with finite ${\rm MBNF}$ theories $\Sigma$ , therefore we refer to a single formula $\sigma$ (which corresponds to the conjunction of all the formulas contained in the finite theory $\Sigma$ ).

Characterizing MBNF Models

We now present a finite characterization of the ${\rm MBNF}$ models of a formula $\sigma\in{\cal L}_M$ . As in several methods for reasoning in nonmonotonic modal logics [12,25,6,28,5], the technique we employ is based on the definition of a correspondence between the preferred models of a theory and the partitions of the set of modal subformulas of the theory. In fact, such partitions can be used in order to provide a finite characterization of a universal Kripke structure: specifically, a partition satisfying certain properties identifies a particular universal Kripke structure M, by uniquely determining a propositional theory such that M is the set of all interpretations satisfying such a theory.

We extend such known techniques in order to deal with the preference semantics of ${\rm MBNF}$ . In particular, we characterize the properties that a partition of modal subformulas of a formula $\sigma\in{\cal L}_M$ must satisfy in order to identify an ${\rm MBNF}$ model for $\sigma$ . In this way, we provide a method that does not rely on a modal logic theorem prover, but reduces the problem of reasoning in a bimodal logic to a number of reasoning problems in propositional logic.

First, we introduce some preliminary definitions. We call a formula of the form $B\varphi$ or ${\it not}\:\varphi$ , with $\varphi \in{\cal L}_M$ , a modal atom.

Observe that only the occurrences in $\sigma$ of modal subformulas which are not within the scope of another modality are replaced; notice also that, if $P\cup N$ contains $MA(\sigma)$ , then $\sigma(P,N)$ is a propositional formula. In this case, the pair (P,N) identifies a guess on the modal subformulas from $\sigma$ , i.e. P contains the modal subformulas of $\sigma$ assumed to hold, while N contains the modal subformulas of $\sigma$ assumed not to hold.

Roughly speaking, the propositional formula ${\it ob}(P,N)$ represents the ``objective knowledge'' implied by the guess (P,N) on the formulas of the form $B\varphi$ belonging to P. From the semantic viewpoint, in each structure (I,M,M') satisfying the guess on the modal atoms given by (P,N), the propositional formula ${\it ob}(P,N)$ constrains the interpretations of M, since in each such structure the propositional formula ${\it ob}(P,N)$ must be satisfied by each interpretation $J\in M$ , i.e. $J\models {\it ob}(P,N)$ .

Proof. Follows immediately from Definitions 4.2 and 4.5, and from the definition of satisfiability in ${\rm MBNF}$ structures. $\Box$

We now show that, if (I,M) is an ${\rm MBNF}$ model for $\sigma$ which induces the partition (P,N) of $MA(\Sigma)$ , then the formula ${\it ob}(P,N)$ completely characterizes the set of interpretations M.

Proof. Let $M'=\{J:J\models{\it ob}(P,N)\}$ . Since (M,M) induces the partition (P,N), by Definition 4.5 it follows that each interpretation in M must satisfy ${\it ob}(P,N)$ , hence $M\subseteq M'$ . Now suppose $M\subset M'$ , and consider the structure (I,M',M). We prove that each modal atom $\xi\in MA(\sigma)$ belongs to P iff $(I,M',M)\models \xi$ . The proof is by induction on the depth of formulas in $MA(\sigma)$ .

First, consider a modal atom ${\it not}\:\psi$ such that $\psi\in{\cal L}$ : from the definition of satisfiability of a formula in an ${\rm MBNF}$ structure, it follows immediately that ${\it not}\:\psi\in P$ iff $(I,M',M)\models{\it not}\:\psi$ . Then, consider a modal atom $B\psi$ such that $\psi\in{\cal L}$ : if $B\psi\in P$ , then, by definition of ${\it ob}(P,N)$ , the propositional formula ${\it ob}(P,N)\supset\psi$ is valid, therefore $(I,M',M)\models B\psi$ . If $B\psi\in N$ , then there exists an interpretation J in M such that $J\not\models \psi$ , and since $M'\supset M$ , it follows that $(I,M',M)\not\models B\psi$ . Hence, each modal atom $\xi\in MA(\sigma)$ of depth 1 belongs to P iff $(I,M',M)\models \xi$ .

Suppose now that $\xi\in P$ iff $(I,M',M)\models \xi$ for each modal atom $\xi$ in $MA(\sigma)$ of depth less or equal to i. Consider a modal atom $B\psi$ of $MA(\sigma)$ of depth i+1: by the induction hypothesis, and by Lemma 4.6, $(I,M',M)\models B\psi$ iff $M'\models B(\psi(P,N))$ . Now, if $B\psi\in P$ , then, by definition of ${\it ob}(P,N)$ , the propositional formula ${\it ob}(P,N)\supset\psi(P,N)$ is valid, and since $M'=\{J:J\models{\it ob}(P,N)\}$ , it follows that $M'\models B(\psi(P,N))$ , which in turn implies $(I,M',M)\models B\psi$ ; on the other hand, if $B\psi\in N$ , then there exists an interpretation J in M such that $(J,M,M)\not\models \psi$ , hence, by the induction hypothesis and Lemma 4.6, $J\not\models \psi(P,N)$ . Now, since $M'\supset M$ , it follows that $M'\not\models B(\psi(P,N))$ , hence $(I,M',M)\not\models B\psi$ . In the same way it is possible to show that a modal atom of the form ${\it not}\:\psi$ of depth i+1 belongs to P iff $(I,M',M)\models{\it not}\:\psi$ .

We have thus proved that each modal atom $\xi\in MA(\sigma)$ belongs to P iff $(I,M',M)\models \xi$ : this in turn implies that $(I,M',M)\models\sigma$ iff $I\models\sigma(P,N)$ , and since by hypothesis (I,M,M) satisfies $\sigma$ and (P,N) is the partition of $MA(\Sigma)$ induced by (M,M), by Lemma 4.6 it follows that $I\models\sigma(P,N)$ . Therefore, $(I,M',M)\models\sigma$ , which contradicts the hypothesis that (I,M) is an ${\rm MBNF}$ model for $\sigma$ . Consequently, M'=M, which proves the thesis. $\Box$

Informally, the above theorem states that each ${\rm MBNF}$ model for $\sigma$ can be associated with a partition (P,N) of the modal atoms of $\sigma$ ; moreover, the propositional formula ${\it ob}(P,N)$ exactly characterizes the set of interpretations M of an ${\rm MBNF}$ model (I,M), in the sense that M is the set of all interpretations satisfying ${\it ob}(P,N)$ . This provides a finite way to describe all ${\rm MBNF}$ models for $\sigma$ .

We now define the notion of a partition of a set of modal atoms induced by a pair of propositional formulas.

In order to simplify notation, we denote as ${\it Prt}(\sigma,\varphi )$ the partition ${\it Prt}(\sigma,\varphi ,\varphi )$ . The following theorem provides a constructive way to build the partition ${\it Prt}(\sigma,\varphi ,\psi)$ .

Theorem 4.9 Let $\sigma\in{\cal L}_M$ , $\varphi ,\psi\in{\cal L}$ . Let (P,N) be the partition of $MA(\sigma)$ built as follows:

1.: start from $P = N = \emptyset$ ;
2.: for each modal atom $B\xi$ in $MA(\sigma)$ such that $\xi(P,N)\in{\cal L}$ , if the propositional formula $\varphi \supset\xi(P,N)$ is valid, then add $B\xi$ to P, otherwise add $B\xi$ to N;
3.: for each modal atom ${\it not}\:\xi$ in $MA(\sigma)$ such that $\xi(P,N)\in{\cal L}$ , if the propositional formula $\psi\supset\xi(P,N)$ is not valid, then add ${\it not}\:\xi$ to P, otherwise add ${\it not}\:\xi$ to N;
4.: iteratively apply the above rules until $P\cup N = MA(\sigma)$ .

Then, $(P,N) = {\it Prt}(\sigma,\varphi ,\psi)$ .

Proof. The proof is by induction on the structure of the formulas in $MA(\sigma)$ . First, from the fact that ${\it Prt}(\sigma,\varphi ,\psi)$ is the partition induced by (M,M'), with $M = \{I : I \models \varphi \}$ , $M' = \{I : I \models \psi \}$ , and from the definition of satisfiability in ${\rm MBNF}$ structures, it follows that, if $\xi\in{\cal L}$ , then $(M,M')\models B\xi$ if and only if $\varphi \supset\xi$ is a valid propositional formula, and $(M,M')\models {\it not}\:\xi$ if and only if $\psi\supset\xi$ is not a valid propositional formula. Therefore, (P,N) agrees with ${\it Prt}(\sigma,\varphi ,\psi)$ on all modal atoms of modal depth 1. Suppose now that (P,N) and ${\it Prt}(\sigma,\varphi ,\psi)$ agree on all modal atoms of modal depth less or equal to i. Consider a modal atom $B\xi$ of $MA(\sigma)$ of modal depth i+1. From Lemma 4.6 and from the definition of satisfiability in ${\rm MBNF}$ structures, it follows that $(M,M')\models B\xi$ if and only if $\varphi \supset\xi({\it Prt}(\sigma,\varphi ,\psi))$ is a valid propositional formula, and since by Definition 4.2 the value of the formula $\xi({\it Prt}(\sigma,\varphi ,\psi))$ only depends on the guess of the modal atoms of modal depth less or equal to i in ${\it Prt}(\sigma,\varphi ,\psi)$ , by the induction hypothesis it follows that $\xi({\it Prt}(\sigma,\varphi ,\psi)) = \xi(P,N)$ , hence $B\xi$ belongs to P if and only if $(M,M')\models B\xi$ . Analogously, it can be proven that any modal atom of depth i+1 of the form ${\it not}\:\xi$ belongs to P if and only if $(M,M')\models {\it not}\:\xi$ . Therefore, (P,N) and ${\it Prt}(\sigma,\varphi ,\psi)$ agree on all modal atoms of modal depth i+1. $\Box$

The algorithms we present in the following for reasoning in ${\rm MBNF}$ use the above shown properties of partitions of modal subformulas of a formula $\sigma$ , together with additional conditions on such partitions (that vary according to the different classes of theories accepted as inputs), in order to identify all the ${\rm MBNF}$ models for $\sigma$ .

As for the entailment problem $\sigma \models_{{\rm MBNF}} \varphi$ , we point out that the occurrences of ${\it not}$ in $\varphi$ are equivalent to occurrences of $\neg B$ , since in each ${\rm MBNF}$ model for $\sigma$ both modalities in $\varphi$ are evaluated on the same set of interpretations. Therefore, as in the original formulation of ${\rm MBNF}$ [22], we restrict query answering in ${\rm MBNF}$ to positive formulas.

Let $\varphi\in{\cal L}_B$ , $\psi\in{\cal L}$ , and $M=\{J : J\models\psi\}$ . We denote as $\varphi (\psi)$ the propositional formula obtained from $\varphi$ by substituting each strict occurrence of a modal atom $B\xi$ of $\varphi$ with $\mbox{{\it true}}$ if $M\models B\xi$ , and with $\mbox{{\it false}}$ otherwise. It can be immediately verified that $\varphi (\psi)=\varphi ({\it Prt}(\varphi ,\psi))$ .

Proof. The proof follows immediately from the fact that, by Theorem 4.9, $\varphi({\it ob}(P,N))=\varphi({\it Prt}(\varphi ,{\it ob}(P,N)))$ , and from Lemma 4.6. $\Box$

We now show that the entailment problem in ${\rm MBNF}$ is related to the membership problem for stable sets [13], which in turn is related to the notion of (objective) kernel that has been used to characterize stable expansions of autoepistemic theories [25].

Proof. Let $M=\{I:I\models{\it ob}(P,N)\}$ : from the above definition and Definition 3.2, it follows immediately that ${\it ST}({\it ob}(P,N))=Th(M)$ . Therefore, if $\varphi\in{\cal L}_B^S$ then $(I,M,M)\models\varphi$ iff $\varphi \in {\it ST}({\it ob}(P,N))$ . $\Box$

Reasoning in Propositional MBNF

We now define a deductive method for reasoning in general propositional ${\rm MBNF}$ theories. Specifically, we present the algorithm MBNF-Not-Entails, reported in Figure 1, for computing entailment in ${\rm MBNF}$ .

**Figure 1:** Algorithm ${\rm MBNF}$ -Not-Entails.
$\begin{figure} \begin{tabbing} {\bf Algorithm} {\rm MBNF}-Not-Entails($\sigma,\v... ...\ {\bf else return} \mbox{{\it false}}\\ {\bf end} \end{tabbing}% \end{figure}$

The algorithm exploits the finite characterization of ${\rm MBNF}$ models given by Theorem 4.7 and an analogous finite characterization, in terms of partitions of $MA(\sigma)$ , of all the models relevant for establishing whether a partition (P,N) of $MA(\sigma)$ identifies an ${\rm MBNF}$ model.

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

Example 4.13 Suppose

$\begin{eqnarray*} \sigma & = & B(a\vee Bb)\wedge ({\it not}(c\vee \neg d)\vee B\... ...e c \\ \varphi & = & \neg B b \vee (\neg b \wedge B(a\wedge b)) \end{eqnarray*}$

Then, $MA(\sigma) = \{ B(a\vee Bb), Bb, {\it not}(c\vee\neg d), B\neg{\it not}\:b, {\it not}\:b \}$ . Now suppose that (P,N)=(P₁,N₁), where

$\begin{eqnarray*} P_1 & = & \{ B(a\vee Bb), {\it not}(c\vee \neg d), {\it not}\:b \} \\ N_1 & = & \{ Bb, B\neg{\it not}\:b \} \end{eqnarray*}$

Then, $\sigma(P,N) = \mbox{{\it true}}\wedge(\mbox{{\it true}}\vee\mbox{{\it false}})\wedge c$ (which is equivalent to c), and ${\it ob}(P,N)= a\vee\mbox{{\it false}}$ (which is equivalent to a). Now, let $M=\{I:I\models a\}$ : it is easy to see that (M,M) satisfies the modal atoms in P, while it does not satisfy the modal atoms in N, hence $(P,N) = {\it Prt}(\Sigma,{\it ob}(P,N))$ , thus satisfying condition (a) of the algorithm. Then, since $a\supset a\wedge b$ is not a valid propositional formula, $M\not\models B(a\wedge b)$ , hence $\neg \varphi ({\it ob}(P,N))= \neg(\mbox{{\it true}}\vee(\neg b \wedge \mbox{{\it false}}))$ , which is equivalent to $\mbox{{\it false}}$ . Therefore, $\sigma(P,N) \wedge \neg \varphi ({\it ob}(P,N))$ is not satisfiable, thus condition (b) does not hold.

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

$\begin{eqnarray*} P_2 & = & \{ B(a\vee Bb), {\it not}(c\vee \neg d), Bb, B\neg{\it not}\:b\}\\ N_2 & = & \{ {\it not}\:b \} \end{eqnarray*}$

Then, $\sigma(P,N) = \mbox{{\it true}}\wedge(\mbox{{\it true}}\vee\mbox{{\it true}})\wedge c$ (which is equivalent to c), and ${\it ob}(P,N)= (a\vee\mbox{{\it true}}) \wedge b \wedge \mbox{{\it true}}$ , which is equivalent to b. Again, it is easy to see that $(P,N) = {\it Prt}(\Sigma,{\it ob}(P,N))$ , thus satisfying condition (a) of the algorithm. Then, since $b\supset a\wedge b$ is not a valid propositional formula, $\neg \varphi ({\it ob}(P,N))= \neg(\mbox{{\it false}}\vee(\neg b \wedge \mbox{{\it false}}))$ , which is equivalent to $\mbox{{\it true}}$ . Hence, $\sigma(P,N) \wedge \neg \varphi ({\it ob}(P,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(\sigma)$ different from (P₂,N₂), with the exception of (P₁,N₁). So let (P',N')=(P₁,N₁): as shown before, ${\it ob}(P',N')$ is equivalent to a, hence ${\it ob}(P,N)\wedge \neg {\it ob}(P',N')$ is equivalent to $b\wedge\neg a$ , therefore condition (c3) holds for (P',N')=(P₁,N₁), which implies that condition (c) holds for (P,N)=(P₂,N₂). Consequently, ${\rm MBNF}$ -Not-Entails( $\sigma,\varphi$ ) returns $\mbox{{\it true}}$ . In fact, the partition (P₂,N₂) identifies the set of ${\rm MBNF}$ models for $\sigma$ (I,M) such that I is an interpretation satisfying c and $M=\{I:I\models b\}$ . Each such model does not satisfy the query $\varphi$ : indeed, it can immediately be verified that, for each interpretation I, $(I,M,M)\not\models\neg Bb \vee (\neg b \wedge B(a\wedge b))$ , since $M\not\models B(a\wedge b)$ and $M\models Bb$ .

To prove correctness of the algorithm ${\rm MBNF}$ -Not-Entails we need the following preliminary lemma.

Proof. The proof is by induction on the depth of the modal atoms of $MA(\Sigma)$ . Let ${\it not}\:\psi\in MA(\Sigma)$ such that $\psi\in{\cal L}$ : then, $(M',M)\models{\it not}\:\psi$ iff there exists an interpretation $I\in M$ such that $I\not\models\psi$ , therefore $(M',M)\models{\it not}\:\psi$ iff $(M'',M)\models {\it not}\:\psi$ . Now let $B\psi\in MA(\Sigma)$ such that $\psi\in{\cal L}$ : by Definition 4.3, $(M',M)\models B\psi$ iff the propositional formula ${\it ob}(P,N)\supset\psi$ is valid, and since $M''=\{I:I\models {\it ob}(P,N)\}$ , it follows that $(M',M)\models B\psi$ iff $(M'',M)\models B\psi$ .

Now suppose that, for each modal atom $\xi$ of depth i, $(M',M)\models \xi$ iff $(M'',M)\models \xi$ , and let (P',N') denote the partition of the modal atoms in $MA(\Sigma)$ of depth less or equal to i induced by (M',M). First, consider a modal atom ${\it not}\:\psi$ of depth i+1. Then, by Lemma 4.6, $(M',M)\models{\it not}\:\psi$ iff $(M',M)\models {\it not}(\psi(P',N'))$ and, by the inductive hypothesis and Lemma 4.6, $(M'',M)\models {\it not}\:\psi$ iff $(M'',M)\models {\it not}(\psi(P',N'))$ . Then, since $\psi$ has depth i, $\psi(P',N')$ is a propositional formula, hence $(M',M)\models {\it not}(\psi(P',N'))$ iff there exists an interpretation $I\in M$ such that $I\not\models\psi(P',N')$ , which immediately implies that $(M',M)\models{\it not}\:\psi$ iff $(M'',M)\models {\it not}\:\psi$ . Now consider a modal atom $B\psi$ of depth i+1. Then, by Lemma 4.6, $(M',M)\models B\psi$ iff $(M',M)\models B(\psi(P',N'))$ and, by the inductive hypothesis and Lemma 4.6, $(M'',M)\models B\psi$ iff $(M'',M)\models B(\psi(P',N'))$ . By Definition 4.3, $(M',M)\models B\psi$ iff the propositional formula ${\it ob}(P,N)\supset\psi(P',N')$ is valid, and since $M''=\{I:I\models {\it ob}(P,N)\}$ , it follows that $(M',M)\models B\psi$ iff $(M'',M)\models B\psi$ , which proves the thesis. $\Box$

Proof. If part. Suppose $\sigma\not\models_{\rm MBNF}\varphi$ . Then, there exists a pair (I,M) such that (I,M) is an ${\rm MBNF}$ model for $\sigma$ and $(I,M,M)\not\models\varphi$ . Let (P,N) be the partition of $MA(\Sigma)$ induced by (M,M). By Theorem 4.7, $M=\{I:I\models{\it ob}(P,N)\}$ . Therefore, by Definition 4.8, $(P,N) = {\it Prt}(\Sigma,{\it ob}(P,N))$ . Then, since $(I,M,M)\not\models\varphi$ , by Theorem 4.10 it follows that $I\not\models\varphi ({\it ob}(P,N))$ , and since $(I,M,M)\models\sigma$ , by Lemma 4.6 $I\models\sigma(P,N)$ , therefore $I\models\sigma(P,N)\wedge\neg\varphi ({\it ob}(P,N))$ . Now suppose there exists a partition (P',N') of $MA(\Sigma)$ such that