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 $(P',N')\neq(P,N)$ and none of conditions (c1), (c2), and (c3) holds. Then, since $\sigma(P',N')$ is satisfiable, there exists an interpretation J such that $J\models \sigma(P',N')$ , and since $(P',N')={\it Prt}(\Sigma,{\it ob}(P',N'),{\it ob}(P,N))$ , from Lemma 4.6 it follows that there exists an interpretation J such that $(J,M',M)\models \sigma$ , where $M'=\{I:I\models {\it ob}(P',N')\}$ . Then, since condition (c3) does not hold, the propositional formula ${\it ob}(P,N)\supset{\it ob}(P',N')$ is valid, which implies that $M'\supseteq M$ . Now, if M'=M, then (P',N') would be the partition induced by (M,M), thus contradicting the hypothesis $(P',N')\neq(P,N)$ . Hence, $M'\supset M$ , and since $(J,M',M)\models \sigma$ , it follows that (I,M) is not an ${\rm MBNF}$ model for $\sigma$ . Contradiction. Consequently, condition (c) in the algorithm holds, therefore MBNF-Not-Entails( $\sigma,\varphi$ ) returns true.

Only-if part. Suppose MBNF-Not-Entails( $\sigma,\varphi$ ) returns true. Then, there exists a partition (P,N) of $MA(\Sigma)$ such that conditions (a), (b), and (c) hold. Let $M=\{I:I\models{\it ob}(P,N)\}$ . Since $(P,N) = {\it Prt}(\Sigma,{\it ob}(P,N))$ , by Definition 4.8 (P,N) is the partition induced by (M,M). And since $\sigma(P,N) \wedge \neg \varphi ({\it ob}(P,N))$ is satisfiable, it follows that there exists an interpretation I such that $I\models\sigma(P,N)$ and $I\not\models\varphi ({\it ob}(P,N))$ , hence, by Lemma 4.6, $(I,M,M)\models\sigma$ and $(I,M,M)\not\models\varphi$ . Now suppose (I,M) is not an ${\rm MBNF}$ model for $\sigma$ . Then, there exists a set M' and an interpretation J such that $M'\supset M$ and $(J,M',M)\models \sigma$ . Let (P',N') be the partition of $MA(\Sigma)$ induced by (M',M). Since $M=\{I:I\models{\it ob}(P,N)\}$ , it follows that M' contains at least one interpretation J which does not satisfy ${\it ob}(P,N)$ , and since ${\it ob}(P,N)=\bigwedge_{B\psi\in P} \psi(P,N)$ , J does not satisfy at least one formula of the form $\psi(P,N)$ such that $B\psi\in P$ . Therefore, $P'\neq P$ , which implies that $(P',N')\neq(P,N)$ . Then, since $(J,M',M)\models \sigma$ , by Lemma 4.6 $J\models \sigma(P',N')$ , hence $\sigma(P',N')$ is satisfiable. Now let $M''=\{I:I\models {\it ob}(P',N')\}$ . By Lemma 4.14, it follows that (P',N') is the partition induced by (M'',M), therefore, by Definition 4.8, $(P',N')={\it Prt}(\Sigma,{\it ob}(P',N'),{\it ob}(P,N))$ . Moreover, since $M'\supset M$ , it follows that the propositional formula ${\it ob}(P,N)\supset{\it ob}(P',N')$ is valid, hence the formula ${\it ob}(P,N)\wedge \neg {\it 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 ${\rm MBNF}$ model for $\sigma$ , and since $(I,M,M)\not\models\varphi$ , it follows that $\sigma\not\models_{\rm MBNF}\varphi$ , thus proving the thesis. $\Box$

We point out the fact that the algorithm ${\rm MBNF}$ -Not-Entails does not rely on a theorem prover for a modal logic: thus, ``modal reasoning'' is not actually needed for reasoning in ${\rm MBNF}$ . This is an interesting peculiarity that ${\rm MBNF}$ shares with other nonmonotonic modal formalisms, like autoepistemic logic [27] or the autoepistemic logic of knowledge [33].

Reasoning in Flat MBNF

We now study reasoning in flat ${\rm MBNF}$ theories. The main reason for taking into account the flat fragment of ${\rm 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 ${\rm MBNF}$ theories [22]. It is known that, if $\sigma\in{\cal L}_M^1$ and $\varphi\in{\cal L}_B^S$ , then it is possible to reduce the entailment $\sigma \models_{{\rm MBNF}} \varphi$ to reasoning in logic ${\bf\sf S4F}_{MDD}$ , by translating ${\rm MBNF}$ formulas into unimodal formulas of ${\bf\sf S4F}_{MDD}$ [37]. Thus, the procedure for deciding entailment in the logic ${\bf\sf S4F}_{MDD}$ presented by [25] can be employed for computing the entailment $\sigma \models_{{\rm MBNF}} \varphi$ . In the following we study a more general problem, that is entailment $\sigma \models_{{\rm MBNF}} \varphi$ in the case $\sigma\in{\cal L}_M^1$ and $\varphi\in{\cal L}_B$ , and present a specialized algorithm for this problem, which is simpler than the more general reasoning method for ${\bf\sf S4F}_{MDD}$ .

In Figure 2 we report the algorithm Flat-Not-Entails for computing such an entailment. In the algorithm, P_n denotes the subset of modal atoms from P prefixed by the modality ${\it not}$ , i.e. $P_n=\{{\it not}\:\psi:{\it not}\:\psi\in P\}$ .

**Figure 2:** Algorithm Flat-Not-Entails.
$\begin{figure} \begin{tabbing} {\bf Algorithm} Flat-Not-Entails($\sigma,\varphi$... ...\ {\bf else return} \mbox{{\it false}}\\ {\bf end} \end{tabbing}% \end{figure}$

Informally, correctness of the algorithm Flat-Not-Entails is established by the fact that, if $\sigma\in{\cal L}_M^1$ , then (a), (b), and (c) are necessary and sufficient conditions on a partition (P,N) in order to establish whether it is induced by a pair (M,M) such that there exists an ${\rm MBNF}$ model for $\sigma$ of the form (I,M). In particular, condition (c) states that $B({\it ob}(P,N))$ must be a consequence of $\sigma(P_n,N)$ in modal logic ${\bf\sf S5}$ ,¹since it can be shown that if $\sigma(P_n,N) \supset B({\it ob}(P,N))$ is not valid in ${\bf\sf S5}$ , then the guess on the modal atoms of the form $B\varphi$ in P is not minimal. We illustrate this fact through the following example.

Example 4.16 Let

$\begin{displaymath}\sigma=(Ba\wedge{\it not}(c\vee d))\vee(B(a\wedge b)\wedge\neg Bc)\vee Bc\end{displaymath}$

and suppose

$\begin{eqnarray*} P & = & \{Ba,B(a\wedge b), {\it not}(c\vee d) \}\\ N & = & \{ Bc\} \end{eqnarray*}$

Then,

$\begin{displaymath}\sigma(P_n,N) = (Ba \wedge \mbox{{\it true}})\vee (B(a\wedge b)\wedge \neg\mbox{{\it false}}) \vee \mbox{{\it false}}, \end{displaymath}$

which is propositionally equivalent to $Ba\vee B(a\wedge b)$ , and ${\it ob}(P,N)=a\wedge(a\wedge b)$ , which is equivalent to $a\wedge b$ . Now, $Ba \vee B(a\wedge b)\supset B(a\wedge b)$ is not valid in ${\bf\sf S5}$ , which is proved by the fact that the set of interpretations $M'=\{I:I\models a\}$ is such that $M'\models(Ba \vee B(a\wedge b))\wedge \neg B(a\wedge b)$ . Indeed, the set of interpretations M' can be immediately used in order to prove that (P,N) does not identify any ${\rm MBNF}$ model for $\sigma$ . In fact, let $M=\{J:J\models a\wedge b\}$ : it is immediate to see that, for each interpretation I, $(I,M',M)\models\sigma$ , and since $M'\supset M$ , (I,M) is not an ${\rm MBNF}$ model for $\sigma$ .

Finally, condition (b) corresponds to check whether there exists an interpretation I satisfying $\neg\varphi ({\it ob}(P,N))$ : in fact, if such an interpretation exists, then (I,M) is an ${\rm MBNF}$ model for $\sigma$ which does not satisfy $\varphi$ .

Therefore, the algorithms ${\rm MBNF}$ -Not-Entails and Flat-Not-Entails only differ in the way in which it is verified whether the ${\rm MBNF}$ structure associated with a partition (P,N) satisfies the preference semantics provided by Definition 2.1, which is implemented through condition (c) in both algorithms. In the algorithm ${\rm MBNF}$ -Not-Entails, a partition is checked against all other partitions of $MA(\sigma)$ , while in the algorithm Flat-Not-Entails it is sufficient to verify that the partition (P,N) satisfies a ``local'' property. As shown in the next section, such a difference reflects the different computational properties of the entailment problem in the two cases.

In order to establish correctness of the algorithm, we need a preliminary lemma.

Proof. Suppose (I,M) is an ${\rm MBNF}$ model for $\sigma$ , and let (P,N) be the partition induced by (M,M). Let M' be any set of interpretations such that $M'\supset M$ . Then, $(M',M)\not\models\sigma$ . Since $\sigma\in{\cal L}_M^1$ and $M'\supset M$ , this implies that for each modal atom $\xi$ in N, $(M',M)\not\models \xi$ . Moreover, for each modal atom ${\it not}\:\psi\in P$ , $(M',M)\models{\it not}\:\psi$ . Therefore, by Lemma 4.6, $(M',M)\not\models\sigma(P_n,N)$ . Now, since $\sigma\in{\cal L}_M^1$ , $\sigma(P_n,N)$ is a flat positive formula, hence its satisfiability only depends on the structure M', therefore $M'\not\models\sigma(P_n,N)$ .

Conversely, suppose (I,M) is not an ${\rm MBNF}$ model for $\sigma$ , and let (P,N) be the partition induced by (M,M). Then, there exists a set of interpretations M' such that $M'\supset M$ and $(M',M)\models\sigma$ . As shown before, this implies that the positive formula $\sigma(P_n,N)$ is satisfied by M'. $\Box$

As observed in Section 2, the class of universal Kripke structures characterizes modal logic ${\bf\sf S5}$ . This immediately implies the following property.

Based on the above property, we are now able to prove correctness of the algorithm Flat-Not-Entails.

Proof. If-part. If $\sigma\not\models_{\rm MBNF}\varphi$ , then there exists an ${\rm MBNF}$ model (I,M) for $\sigma$ such that $(I,M,M)\not\models\varphi$ . Let (P,N) be the partition of $MA(\sigma)$ induced by (M,M). From Theorem 4.7 it follows that $M=\{J:J\models{\it ob}(P,N)\}$ . Therefore, by Definition 4.8, $(P,N) = {\it Prt}(\Sigma,{\it ob}(P,N))$ , hence condition (a) in the algorithm holds.

Now let $\sigma'=\sigma(P_n,N)$ , and suppose the formula $\sigma'\supset B({\it ob}(P,N))$ is not valid in ${\bf\sf S5}$ . Then, since the formula $\sigma'\supset B({\it ob}(P,N))$ belongs to ${\cal L}_B^S$ , by Lemma 4.18 it follows that there exists a set of interpretations M' satisfying $\sigma'\wedge\neg B({\it ob}(P,N))$ . Let (P',N') be the partition of $MA(\sigma')$ induced by (M',M'), and let $M''=\{I:I\models {\it ob}(P',N')\}$ . Since ${\it ob}(P,N)=\bigwedge_{B\varphi \in MA(\sigma')}\varphi$ , by Definition 4.3 it follows that ${\it ob}(P,N)\supset{\it ob}(P',N')$ is a valid propositional formula, hence $M''\supseteq M$ . Now, since by hypothesis $M'\models\neg B({\it ob}(P,N))$ , it follows that $M''\supset M$ . Moreover, since $\sigma'\in{\cal L}_B$ , by Lemma 4.14 it follows that (P',N') is the partition induced by (M'',M''), and since $M'\models\sigma'$ and $\sigma'$ is flat, $\sigma'(P',N')$ is equivalent to $\mbox{{\it true}}$ , therefore $M''\models\sigma'(P',N')$ and, by Lemma 4.6, $M''\models\sigma'$ . On the other hand, since $M''\supset M$ , by Lemma 4.17 it follows that $M''\not\models\sigma'$ . Contradiction. Hence, $\sigma'\supset B({\it ob}(P,N))$ is valid in ${\bf\sf S5}$ , consequently condition (c) of the algorithm holds.

Finally, since $(I,M,M)\not\models\varphi$ and $M=\{J:J\models{\it ob}(P,N)\}$ , by Theorem 4.10 it follows that $I\not\models\varphi ({\it ob}(P,N))$ . Moreover, since $(I,M,M)\models\sigma$ , from Lemma 4.6 it follows that $I\models\sigma(P,N)$ , consequently $I\models\sigma(P,N)\wedge\neg\varphi ({\it ob}(P,N))$ , hence the propositional formula $\sigma(P,N) \wedge \neg \varphi ({\it ob}(P,N))$ is satisfiable. Therefore, conditions (a), (b), and (c) in the algorithm hold, which implies that Flat-Not-Entails( $\sigma,\varphi$ ) returns true.

Only-if-part. If Flat-Not-Entails( $\sigma,\varphi$ ) returns true, then there exists a partition (P,N) of $MA(\sigma)$ for which conditions (a), (b), and (c) of the algorithm hold. Let $M=\{J:J\models{\it ob}(P,N)\}$ . By Definition 4.8, (P,N) is the partition of $MA(\sigma)$ induced by (M,M). Now, since $\sigma(P,N) \wedge \neg \varphi ({\it ob}(P,N))$ is satisfiable, there exists an interpretation I such that $I\models\sigma(P,N)$ and $I\models\neg\varphi({\it ob}(P,N))$ , hence by Lemma 4.6 $(I,M,M)\models\sigma$ , and by Theorem 4.10 $(I,M,M)\not\models\varphi$ , therefore we only have to show that (I,M) is an ${\rm MBNF}$ model for $\sigma$ . So, let us suppose (I,M) is not an ${\rm MBNF}$ model for $\sigma$ . Then, by Lemma 4.17 there exists $M'\supset M$ such that $\sigma(P_n,N)$ is satisfied in M'. Now, condition (c) in the algorithm implies that $B({\it ob}(P,N))$ is a consequence of $\sigma(P_n,N)$ in ${\bf\sf S5}$ , therefore ${\it ob}(P,N)$ is satisfied by each interpretation in M', that is, $M'\subseteq\{J:J\models {\it ob}(P,N)\}$ , which contradicts the hypothesis $M'\supset M=\{J:J\models {\it ob}(P,N)\}$ . Consequently, (I,M) is an ${\rm MBNF}$ model for $\sigma$ . $\Box$

We remark the fact that the algorithm Flat-Not-Entails can be seen as a generalization of known methods for query answering in Reiter's default logic, Moore's autoepistemic logic, and (disjunctive) logic programming under the stable model (and answer set) semantics. In particular, condition (c) in the algorithm can be seen as a generalization of the minimality check used in (disjunctive) logic programming for verifying stability of a model of a logic program [10,11].

Complexity Results

In this section we provide a computational characterization of reasoning in ${\rm MBNF}$ .

We first briefly recall the complexity classes in the polynomial hierarchy, and refer to [18,29] for further details about the complexity classes mentioned in the paper. P^A (NP^A) is the class of problems that are solved in polynomial time by deterministic (nondeterministic) Turing machines using an oracle for A (i.e. that solves in constant time any problem in A). The classes $\Sigma^p_k$ , $\Pi^p_k$ and $\Delta^p_k$ of the polynomial hierarchy are defined by $\Sigma^p_0 = \Pi^p_0 = \Delta^p_0 =$ P, and for $k \geq 0$ , $\Sigma^p_{k+1} = {\rm NP}^{\Sigma^p_k}$ , $\Pi^p_{k+1} = {\rm co}\Sigma^p_{k+1}$ and $\Delta^p_{k+1} = {\rm P}^{\Sigma^p_k}$ . In particular, the complexity class $\Sigma^p_2$ is the class of problems that are solved in polynomial time by a nondeterministic Turing machine that uses an NP-oracle, and $\Pi^p_2$ is the class of problems that are complement of a problem in $\Sigma^p_2$ , while $\Sigma^p_3$ is the class of problems that are solved in polynomial time by a nondeterministic Turing machine that uses an $\Sigma^p_2$ -oracle, and $\Pi^p_3$ is the class of problems that are complement of a problem in $\Sigma^p_3$ . It is generally assumed that the polynomial hierarchy does not collapse: hence, a problem in the class $\Sigma^p_2$ or $\Pi^p_2$ is considered computationally easier than a $\Sigma^p_3$ -hard or $\Pi^p_3$ -hard problem.

As for the complexity of entailment in ${\rm MBNF}$ , we start by establishing a lower bound for reasoning in propositional ${\rm MBNF}$ theories. To this end, we exploit the correspondence between ${\rm MBNF}$ and the logic of minimal knowledge ${\bf\sf S5}_G$ [14]. Indeed, as stated by Proposition 2.5, there is a one-to-one correspondence between ${\rm MBNF}$ models and ${\bf\sf S5}_G$ models of positive subjective theories.

Proof. As shown by [5], entailment in ${\bf\sf S5}_G$ is $\Pi^p_3$ -complete. Therefore, by Proposition 2.5, for subjective (and hence for general) ${\rm MBNF}$ theories, entailment is $\Pi^p_3$ -hard. $\Box$

Then, we show that the entailment problem in propositional ${\rm MBNF}$ is complete with respect to the class $\Pi^p_3$ .

Proof. Hardness with respect to $\Pi^p_3$ follows from Lemma 5.1. As for membership in $\Pi^p_3$ , we analyze the complexity of the algorithm ${\rm MBNF}$ -Not-Entails reported in Figure 1. In particular, observe that:

Since the guess of the partition (P,N) of $MA(\sigma)$ requires a nondeterministic choice, it follows that the algorithm ${\rm MBNF}$ -Not-Entails, if considered as a nondeterministic procedure, decides $\sigma\not\models_{\rm MBNF}\varphi$ in nondeterministic polynomial time (with respect to the size of $\sigma\wedge\varphi$ ), using a $\Sigma^p_2$ -oracle. Thus, we obtain an upper bound of $\Sigma^p_3$ for the non-entailment problem, which implies that entailment in ${\rm MBNF}$ is in $\Pi^p_3$ . $\Box$

The previous analysis also allows for a computational characterization of the logic ${\rm MKNF}$ [21], which is a slight modification of ${\rm MBNF}$ . Indeed, it is known [22] that, for each theory $\Sigma\subseteq{\cal L}_M$ , M is an ${\rm MKNF}$ model of $\Sigma$ iff, for each interpretation I, (I,M) is an ${\rm MBNF}$ model of the subjective theory $\Sigma'=\{B\varphi\,:\,\varphi\in\Sigma\}$ . Therefore, from Proposition 2.5 and from $\Pi^p_3$ -hardness of entailment in ${\bf\sf S5}_G$ [5], it follows that entailment in ${\rm MKNF}$ is $\Pi^p_3$ -hard. Then, since $\Sigma\models_{{\rm MKNF}}\varphi$ iff $\Sigma'\models_{{\rm MBNF}}B\varphi$ [22], it follows that entailment in ${\rm MKNF}$ can be polynomially reduced to entailment in ${\rm MBNF}$ , hence such a problem belongs to $\Pi^p_3$ . Therefore, the following property holds.

Finally, the previous theorem provides a computational characterization of the logic of grounded knowledge and justified assumptions GK [24]. In fact, the logic GK can be considered as a syntactic variant of the propositional fragment of ${\rm MKNF}$ . Therefore, skeptical entailment in GK is $\Pi^p_3$ -complete.

Remark. The computational properties of ${\rm MBNF}$ and its variants relate such formalisms to ground nonmonotonic modal logics [6,5,32]. Notably, ground nonmonotonic modal logics share with ${\rm MBNF}$ the interpretation in terms of minimal knowledge (or minimal belief) of the modality B; specifically, as already mentioned, the propositional fragment of ${\rm MBNF}$ can be considered as built upon ${\bf\sf S5}_G$ by adding a second modality ${\it not}$ . Therefore, it turns out that, in the propositional case, adding a ``negation by default'' modality to the ${\bf\sf S5}$ logic of minimal knowledge does not increase the computational complexity of reasoning, while adding a minimal knowledge modality to ${\rm AEL}$ does increase the complexity of deduction. We can thus summarize as follows: minimal knowledge is computationally harder than negation as failure. $\Box$

We now study the complexity of entailment for flat ${\rm MBNF}$ theories. First, it is known that, in the case of flat ${\rm MBNF}$ theories and subjective queries, entailment is $\Pi^p_2$ -complete: membership in the class $\Pi^p_2$ is a consequence of the fact that flat ${\rm MKNF}$ theories can be polynomially embedded into McDermott and Doyle's nonmonotonic modal logic ${\bf\sf S4F}$ [37, Proposition 3.2], whose entailment problem is $\Pi^p_2$ -complete [25], while $\Pi^p_2$ -hardness follows from the existence of a polynomial-time embedding of propositional default theories into flat ${\rm MBNF}$ theories [22]. Therefore, the following property holds.

As for complexity of entailment of generic queries with respect to flat ${\rm MBNF}$ theories, we analyze the complexity of the algorithm Flat-Not-Entails reported in Figure 2. As shown before, both condition (a) and condition (b) can be checked through a linear number (with respect to the size of the input) of calls to an NP-oracle. Moreover, validity in modal logic ${\bf\sf S5}$ is a coNP-complete problem [15]. Hence, each of the conditions in the algorithm can be computed through a number of calls to an oracle for the propositional validity problem which is polynomial in the size of the input, and since the guess of the partition (P,N) of $MA(\sigma)$ requires a nondeterministic choice, it follows that the algorithm runs in $\Sigma^p_2$ . Therefore, the following property holds.

Proof. Membership of the problem to the class $\Pi^p_2$ is implied by the algorithm Flat-not-entails, whereas $\Pi^p_2$ -hardness is implied by Proposition 5.4. $\Box$

Hence, the algorithm Flat-Not-Entails is ``optimal'' in the sense that it matches the lower bound for the entailment problem.

Finally, we remark that the subset of flat ${\rm MBNF}$ theories in conjunctive normal form can be seen as a further extension of the framework of generalized logic programming introduced by [16], which in turn is an extension of the disjunctive logic programming framework under the stable model semantics [11]. Roughly speaking, flat ${\rm MBNF}$ theories in conjunctive normal form correspond to rules of generalized logic programs in which propositional formulas (instead of literals) are allowed as goals. The above computational characterization implies that such an extension of the framework of logic programming under the stable model semantics does not affect the worst-case complexity of the entailment problem, which is $\Pi^p_2$ -complete just like entailment in logic programs with disjunction under the stable model semantics [8]. Such a result extends analogous properties [26] to the case of disjunctive logic programs.

Conclusions

In this paper we have investigated the problem of reasoning in the propositional fragment of ${\rm MBNF}$ . The main results presented can be summarized as follows:

As for the computational aspects of reasoning in ${\rm MBNF}$ , the results presented in Section 5 prove that one source of complexity is due to the presence of nested occurrences of modalities in the theory, since reasoning in flat ${\rm MBNF}$ is computationally easier than in the general case.

It can be proven that another source of complexity lies in the underlying objective language. In fact, if we consider ${\cal L}'$ to be a tractable fragment of propositional logic, then the complexity of reasoning in the modal language ${\cal L}_M'$ built upon ${\cal L}'$ is lower than in the general case. In particular, it is easy to see that, under the assumption that entailment in ${\cal L}'$ can be computed in polynomial time, the algorithm ${\rm MBNF}$ -Not-Entails provides an upper bound of $\Pi^p_2$ for ${\rm MBNF}$ -entailment in the fragment ${\cal L}_M'$ .

One possible development of the present work is towards the analysis of reasoning about minimal belief and negation as failure in a first-order setting: in particular, it should be interesting to see whether it is possible to extend the techniques developed for the propositional case to a more expressive language. A first attempt in this direction is reported in [4].

Acknowledgments

This research has been partially supported by Consiglio Nazionale delle Ricerche, grant 203.15.10.