Journal of Artificial Intelligence Research 11 (1999), pp. 277-300. Submitted 5/99; published 10/99.

# 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 , 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 . In particular, we show that skeptical entailment in propositional is -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 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 [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 . The logic thus obtained is characterized in terms of a nice model-theoretic semantics. 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, 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], 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 have been thoroughly investigated [36,3,2], the existing studies concerning the computational properties of are limited to subclasses of propositional 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 . In particular, we show that logical implication in the propositional fragment of is a -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 theories, i.e. theories without nested occurrences of modalities, showing that in this case logical implication is -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 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 exactly corresponds to negative introspection in autoepistemic logic [27]. This result implies that the logic 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 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 . The interest in defining deductive methods for 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 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 . In Section 3 we address the relationship between and Moore's autoepistemic logic. Then, in Section 4 we study the problem of reasoning in propositional : we first consider the case of general theories, then we deal with flat theories. In Section 5 we present the computational characterization of reasoning in . 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 [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 . We use to denote a fixed propositional language built in the usual way from: (i) an alphabet of propositional symbols; (ii) the symbols , ; (iii) the propositional connectives . We denote as the modal extension of with the modalities B and . We say that a formula has (modal) depth i (with ) if each subformula in lies within the scope of at most i modalities, and there exists a subformula in which lies within the scope of exactly i modalities.

We denote as the set of subjective formulas, i.e. the subset of formulas from in which each occurrence of a propositional symbol lies within the scope of at least one modality, and with the set of flat formulas, that is the set of formulas from in which each propositional symbol lies within the scope of exactly one modality. We call a modal formula from positive (resp. negative) if the modality (resp. B) does not occur in . denotes the set of positive formulas from , while denotes the set of positive formulas from .

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

1.
if is a propositional symbol, is satisfied by (I,Mb,Mn) iff ;
2.
is satisfied by (I,Mb,Mn) iff is not satisfied by (I,Mb,Mn);
3.
is satisfied by (I,Mb,Mn) iff is satisfied by (I,Mb,Mn) and is satisfied by (I,Mb,Mn);
4.
is satisfied by (I,Mb,Mn) iff either is satisfied by (I,Mb,Mn) or is satisfied by (I,Mb,Mn);
5.
is satisfied by (I,Mb,Mn) iff either is not satisfied by (I,Mb,Mn) or is satisfied by (I,Mb,Mn);
6.
is satisfied by (I,Mb,Mn) iff, for every , is satisfied by (J,Mb,Mn);
7.
is satisfied by (I,Mb,Mn) iff there exists such that is not satisfied by (J,Mb,Mn).

We write to indicate that is satisfied by (I,Mb,Mn). We say that a theory is satisfied by (I,Mb,Mn) (and write ) iff each formula from is satisfied by (I,Mb,Mn). If , then the evaluation of is insensitive to the initial interpretation I: thus, in this case we also write . Analogously, if , then the evaluation of is insensitive both to the initial interpretation I and to the set Mn, and we also write . If then the evaluation of does not depend on the sets Mb,Mn, and in this case we write .

In order to relate 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 Mb, Mn in an 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 [25, Theorem 7.52].

The nonmonotonic character of is obtained by imposing the following preference semantics over the interpretation structures satisfying a given theory.

Definition 2.1   A structure (I,M,M), where , is an model of a theory iff and, for each interpretation J and for each set of interpretations M', if then .

We say that a formula is entailed (or logically implied) by in (and write ) iff is satisfied by every model of . In order to simplify notation, we denote the model (I,M,M) with the pair (I,M), and, if , we denote (I,M,M) with M, since in this case the evaluation of is insensitive to the initial world I, namely, if (I,M) is a model for , then, for each interpretation J, (J,M) is a model for .

Example 2.2   Let . The only MBNF models for are of the form (I,M), with . Hence, , and for each such that the propositional formula is not valid. Therefore, the agent modeled by has minimal belief, in the sense that she only believes p and the objective facts logically implied by p.

Example 2.3   Let . It is easy to see that the only models for are of the form (I,M) such that , since can be assumed not to hold by the agent modeled by , which is then able to conclude . Notably, the meaning of is analogous to the default rule in Reiter's default logic [22]. Also, let . In a way analogous to the previous case, it can be shown that the only MBNF models for are of the form (I,M), with . Therefore, . As shown by [22], corresponds to the default theory .

Given a set of interpretations M, Th(M) denotes the set of formulas such that and . Let M1,M2 be sets of interpretations. We say that M1 is equivalent to M2 iff Th(M1)=Th(M2).

Definition 2.4   A set of interpretations M is maximal iff, for each set of interpretations M', if M' is equivalent to M then .

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 [19,5]. In fact, is obtained from modal logic by imposing the following preference order over the universal Kripke structures satisfying a theory : M is a model for iff and, for each M', if then [38]. In fact, it is immediate to see that the semantics of theories composed of subjective positive formulas corresponds to the above semantics according to . Hence, the following property holds.

Proposition 2.5   Let . Then, M is an model for iff, for each I, (I,M) is an model for .

The previous proposition implies that, when , a set of interpretations M satisfying is compared with all other sets of interpretations satisfying , while, in the case , M is only compared with the sets M' such that (M',M) satisfies .

Hence, the main difference between MBNF and lies in the fact that in 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 has two types of models, for each possible choice of the initial world J: (J,M1), where M1 corresponds to the set of all interpretations (which represents the case in which is not assumed to hold); and (J,M2), where . Namely, if is assumed to hold, then forces one to conclude : 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 operator B exactly corresponds to the interpretation of the modality B in .

# Relating MBNF to Autoepistemic Logic

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

Definition 3.1   A propositionally consistent set of formulas is a stable expansion for a set of initial knowledge if T satisfies the following equation:
 (1)

where Cn(S) denotes the propositional deductive closure of the modal theory .

Given a theory and a formula , we write iff belongs to all the stable expansions of . Each stable expansion T is a stable set according to the following definition [39].

Definition 3.2   A modal theory is a stable set if
1.
T=Cn(T);
2.
for every , if then ;
3.
for every , if then .

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

Finally, notice that we have adopted the notion of consistent autoepistemic logic [25], i.e. in (1) we do not allow the inconsistent theory 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 , allowing in Definition 2.1 the empty set of interpretations to be a possible component of structures.

In the following, we use the term embedding (or translation) to indicate a transformation function for modal theories. We are interested in finding a faithful embedding [13,35,17], in the following sense: is a faithful embedding of into if, for each theory and for each model M, M is an model for iff M is an model for .

It is already known that theories can be embedded into theories. In particular, it has been proven [24,37] that theories with no nested occurrences of B (called flat theories) can be embedded into ; now, since in 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 theory can be embedded into .

However, we now prove a much stronger result: negation as failure in exactly corresponds to negative introspection in , i.e. 's modality and 's modality 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 theory into .

We first define the translation of modal theories from to theories.

Definition 3.3   Let . Then, is the formula obtained from by substituting each occurrence of B with . Moreover, if , then denotes the theory .

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

Proposition 3.4   [34, Proposition 4.1] Let . Then, M is an model for iff, for each interpretation , and, for each interpretation , .

In the following, we say that an occurrence of a subformula in a formula is strict if it does not lie within the scope of a modal operator. E.g., let . The occurrence of in is strict, while the occurrence of is not strict.

Theorem 3.5   Let . Then, M is an model for iff, for each I, (I,M) is an model of .

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

Only-if part. Suppose M is an model for . Then, by Proposition 3.4, for each interpretation , and, for each interpretation , . For each , let denote the propositional formula obtained from by replacing each strict occurrence of a formula of the form with if and with otherwise, and let . Then, suppose there exists an interpretation J such that and . Then, from the definition of satisfiability in structures it follows that , thus contradicting the hypothesis that M is an AEL model for . Hence, . Now suppose that, for some interpretation I, (I,M) is not an MBNF model for . Then, there exists such that . From the definition of , it follows that each interpretation in M' satisfies , and, since , there exists such that . Contradiction. Therefore, (I,M) is an MBNF model for .

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

The previous theorem implies that the interpretation of the modality in and of the modal operator in autoepistemic logic are the same. This property extends previous results relating with [24,36,3], and has interesting consequences both in the logic programming framework and in nonmonotonic reasoning. In particular, since generalizes the stable model semantics for logic programs [9], the above result strengthens the idea that 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 and in the logic of minimal knowledge [14]: consequently, the logic generalizes both Halpern and Moses' and Moore's .

# Reasoning in MBNF

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

## Characterizing MBNF Models

We now present a finite characterization of the models of a formula . 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 . In particular, we characterize the properties that a partition of modal subformulas of a formula must satisfy in order to identify an model for . 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 or , with , a modal atom.

Definition 4.1   Let . We call the set of modal atoms occurring in the modal atoms of (and denote such a set as ).

Definition 4.2   Let and let (P,N) be a partition of a set of modal atoms. We denote as the formula obtained from by substituting each strict occurrence in of a formula in P with , and each strict occurrence in of a formula in N with .

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

Definition 4.3   Let and let (P,N) be a partition of . We denote as the propositional formula

Roughly speaking, the propositional formula represents the objective knowledge'' implied by the guess (P,N) on the formulas of the form 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 constrains the interpretations of M, since in each such structure the propositional formula must be satisfied by each interpretation , i.e. .

Example 4.4   Let

Then, . Now suppose that

Then, (which is equivalent to d), and .

Definition 4.5   We say that a pair of sets of interpretations (M,M') induces the partition (P,N) of if, for each modal atom , iff .

Lemma 4.6   Let , let I be an interpretation, let M,M' be sets of interpretations, and let (P,N) be the partition induced by (M,M') on a set of modal atoms S. Then, iff .

Proof. Follows immediately from Definitions 4.2 and 4.5, and from the definition of satisfiability in structures.

We now show that, if (I,M) is an model for which induces the partition (P,N) of , then the formula completely characterizes the set of interpretations M.

Theorem 4.7   Let , let (I,M) be an model for , and let (P,N) be the partition of induced by (M,M). Then, .

Proof. Let . Since (M,M) induces the partition (P,N), by Definition 4.5 it follows that each interpretation in M must satisfy , hence . Now suppose , and consider the structure (I,M',M). We prove that each modal atom belongs to P iff . The proof is by induction on the depth of formulas in .

First, consider a modal atom such that : from the definition of satisfiability of a formula in an structure, it follows immediately that iff . Then, consider a modal atom such that : if , then, by definition of , the propositional formula is valid, therefore . If , then there exists an interpretation J in M such that , and since , it follows that . Hence, each modal atom of depth 1 belongs to P iff .

Suppose now that iff for each modal atom in of depth less or equal to i. Consider a modal atom of of depth i+1: by the induction hypothesis, and by Lemma 4.6, iff . Now, if , then, by definition of , the propositional formula is valid, and since , it follows that , which in turn implies ; on the other hand, if , then there exists an interpretation J in M such that , hence, by the induction hypothesis and Lemma 4.6, . Now, since , it follows that , hence . In the same way it is possible to show that a modal atom of the form of depth i+1 belongs to P iff .

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

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

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

Definition 4.8   Let , . We denote as the partition of induced by (M1,M2), where , .

In order to simplify notation, we denote as the partition . The following theorem provides a constructive way to build the partition .

Theorem 4.9   Let , . Let (P,N) be the partition of built as follows:
1.
start from ;
2.
for each modal atom in such that , if the propositional formula is valid, then add to P, otherwise add to N;
3.
for each modal atom in such that , if the propositional formula is not valid, then add to P, otherwise add to N;
4.
iteratively apply the above rules until .
Then, .

Proof. The proof is by induction on the structure of the formulas in . First, from the fact that is the partition induced by (M,M'), with , , and from the definition of satisfiability in structures, it follows that, if , then if and only if is a valid propositional formula, and if and only if is not a valid propositional formula. Therefore, (P,N) agrees with on all modal atoms of modal depth 1. Suppose now that (P,N) and agree on all modal atoms of modal depth less or equal to i. Consider a modal atom of of modal depth i+1. From Lemma 4.6 and from the definition of satisfiability in structures, it follows that if and only if is a valid propositional formula, and since by Definition 4.2 the value of the formula only depends on the guess of the modal atoms of modal depth less or equal to i in , by the induction hypothesis it follows that , hence belongs to P if and only if . Analogously, it can be proven that any modal atom of depth i+1 of the form belongs to P if and only if . Therefore, (P,N) and agree on all modal atoms of modal depth i+1.

The algorithms we present in the following for reasoning in use the above shown properties of partitions of modal subformulas of a formula , 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 models for .

As for the entailment problem , we point out that the occurrences of in are equivalent to occurrences of , since in each model for both modalities in are evaluated on the same set of interpretations. Therefore, as in the original formulation of [22], we restrict query answering in to positive formulas.

Let , , and . We denote as the propositional formula obtained from by substituting each strict occurrence of a modal atom of with if , and with otherwise. It can be immediately verified that .

Theorem 4.10   Let . Let (I,M) be an model for and let (P,N) be the partition of induced by (M,M). Then, is satisfied by (I,M,M) iff .

Proof. The proof follows immediately from the fact that, by Theorem 4.9, , and from Lemma 4.6.

We now show that the entailment problem in 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].

Definition 4.11   Let . We denote as the (unique) stable set such that

Theorem 4.12   Let , . Then, iff there exists an model (I,M) for such that , where (P,N) is the partition of induced by (M,M).

Proof. Let : from the above definition and Definition 3.2, it follows immediately that . Therefore, if then iff .

## Reasoning in Propositional MBNF

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

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

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

We illustrate the algorithm through the following simple example.

Example 4.13   Suppose

Then, . Now suppose that (P,N)=(P1,N1), where

Then, (which is equivalent to c), and (which is equivalent to a). Now, let : 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 , thus satisfying condition (a) of the algorithm. Then, since is not a valid propositional formula, , hence , which is equivalent to . Therefore, is not satisfiable, thus condition (b) does not hold.

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

Then, (which is equivalent to c), and , which is equivalent to b. Again, it is easy to see that , thus satisfying condition (a) of the algorithm. Then, since is not a valid propositional formula, , which is equivalent to . Hence, 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 different from (P2,N2), with the exception of (P1,N1). So let (P',N')=(P1,N1): as shown before, is equivalent to a, hence is equivalent to , therefore condition (c3) holds for (P',N')=(P1,N1), which implies that condition (c) holds for (P,N)=(P2,N2). Consequently, -Not-Entails( ) returns . In fact, the partition (P2,N2) identifies the set of models for (I,M) such that I is an interpretation satisfying c and . Each such model does not satisfy the query : indeed, it can immediately be verified that, for each interpretation I, , since and .

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

Lemma 4.14   Let , and let (P,N) be the partition of induced by (M',M). Let . Then, (P,N) is the partition induced by (M'',M).

Proof. The proof is by induction on the depth of the modal atoms of . Let such that : then, iff there exists an interpretation such that , therefore iff . Now let such that : by Definition 4.3, iff the propositional formula is valid, and since , it follows that iff .

Now suppose that, for each modal atom of depth i, iff , and let (P',N') denote the partition of the modal atoms in of depth less or equal to i induced by (M',M). First, consider a modal atom of depth i+1. Then, by Lemma 4.6, iff and, by the inductive hypothesis and Lemma 4.6, iff . Then, since has depth i, is a propositional formula, hence iff there exists an interpretation such that , which immediately implies that iff . Now consider a modal atom of depth i+1. Then, by Lemma 4.6, iff and, by the inductive hypothesis and Lemma 4.6, iff . By Definition 4.3, iff the propositional formula is valid, and since , it follows that iff , which proves the thesis.

We are now ready to prove correctness of the algorithm MBNF-Not-Entails.

Theorem 4.15   Let , . Then, -Not-Entails( ) returns iff .

Proof. If part. Suppose . Then, there exists a pair (I,M) such that (I,M) is an model for and . Let (P,N) be the partition of induced by (M,M). By Theorem 4.7, . Therefore, by Definition 4.8, . Then, since , by Theorem 4.10 it follows that , and since , by Lemma 4.6 , therefore . Now suppose there exists a partition (P',N') of such that and none of conditions (c1), (c2), and (c3) holds. Then, since is satisfiable, there exists an interpretation J such that , and since , from Lemma 4.6 it follows that there exists an interpretation J such that , where . Then, since condition (c3) does not hold, the propositional formula is valid, which implies that . Now, if M'=M, then (P',N') would be the partition induced by (M,M), thus contradicting the hypothesis . Hence, , and since , it follows that (I,M) is not an model for . Contradiction. Consequently, condition (c) in the algorithm holds, therefore MBNF-Not-Entails( ) returns true.

Only-if part. Suppose MBNF-Not-Entails( ) returns true. Then, there exists a partition (P,N) of such that conditions (a), (b), and (c) hold. Let . Since , by Definition 4.8 (P,N) is the partition induced by (M,M). And since is satisfiable, it follows that there exists an interpretation I such that and , hence, by Lemma 4.6, and . Now suppose (I,M) is not an model for . Then, there exists a set M' and an interpretation J such that and . Let (P',N') be the partition of induced by (M',M). Since , it follows that M' contains at least one interpretation J which does not satisfy , and since , J does not satisfy at least one formula of the form such that . Therefore, , which implies that . Then, since , by Lemma 4.6 , hence is satisfiable. Now let . By Lemma 4.14, it follows that (P',N') is the partition induced by (M'',M), therefore, by Definition 4.8, . Moreover, since , it follows that the propositional formula is valid, hence the formula is unsatisfiable. Consequently, (P',N') does not satisfy condition (c) in the algorithm, thus contradicting the hypothesis. Therefore, (I,M) is an model for , and since , it follows that , thus proving the thesis.

We point out the fact that the algorithm -Not-Entails does not rely on a theorem prover for a modal logic: thus, modal reasoning'' is not actually needed for reasoning in . This is an interesting peculiarity that 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 theories. The main reason for taking into account the flat fragment of 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 theories [22]. It is known that, if and , then it is possible to reduce the entailment to reasoning in logic , by translating formulas into unimodal formulas of [37]. Thus, the procedure for deciding entailment in the logic presented by [25] can be employed for computing the entailment . In the following we study a more general problem, that is entailment in the case and , and present a specialized algorithm for this problem, which is simpler than the more general reasoning method for .

In Figure 2 we report the algorithm Flat-Not-Entails for computing such an entailment. In the algorithm, Pn denotes the subset of modal atoms from P prefixed by the modality , i.e. .

Informally, correctness of the algorithm Flat-Not-Entails is established by the fact that, if , 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 model for of the form (I,M). In particular, condition (c) states that must be a consequence of in modal logic ,1since it can be shown that if is not valid in , then the guess on the modal atoms of the form in P is not minimal. We illustrate this fact through the following example.

Example 4.16   Let

and suppose

Then,

which is propositionally equivalent to , and , which is equivalent to . Now, is not valid in , which is proved by the fact that the set of interpretations is such that . Indeed, the set of interpretations M' can be immediately used in order to prove that (P,N) does not identify any model for . In fact, let : it is immediate to see that, for each interpretation I, , and since , (I,M) is not an model for .

Finally, condition (b) corresponds to check whether there exists an interpretation I satisfying : in fact, if such an interpretation exists, then (I,M) is an model for which does not satisfy .

Therefore, the algorithms -Not-Entails and Flat-Not-Entails only differ in the way in which it is verified whether the 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 -Not-Entails, a partition is checked against all other partitions of , 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.

Lemma 4.17   Let and let (P,N) be the partition induced by a structure (M,M). Then, (I,M) is an model for iff for each the positive formula is not satisfied by M'.

Proof. Suppose (I,M) is an model for , and let (P,N) be the partition induced by (M,M). Let M' be any set of interpretations such that . Then, . Since and , this implies that for each modal atom in N, . Moreover, for each modal atom , . Therefore, by Lemma 4.6, . Now, since , is a flat positive formula, hence its satisfiability only depends on the structure M', therefore .

Conversely, suppose (I,M) is not an model for , and let (P,N) be the partition induced by (M,M). Then, there exists a set of interpretations M' such that and . As shown before, this implies that the positive formula is satisfied by M'.

As observed in Section 2, the class of universal Kripke structures characterizes modal logic . This immediately implies the following property.

Lemma 4.18   A formula is valid in iff, for each set of interpretations M, the formula is not satisfied by M.

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

Theorem 4.19   Let and . Then, Flat-Not-Entails( ) returns true iff .

Proof. If-part. If , then there exists an model (I,M) for such that . Let (P,N) be the partition of induced by (M,M). From Theorem 4.7 it follows that . Therefore, by Definition 4.8, , hence condition (a) in the algorithm holds.

Now let , and suppose the formula is not valid in . Then, since the formula belongs to , by Lemma 4.18 it follows that there exists a set of interpretations M' satisfying . Let (P',N') be the partition of induced by (M',M'), and let . Since , by Definition 4.3 it follows that is a valid propositional formula, hence . Now, since by hypothesis , it follows that . Moreover, since , by Lemma 4.14 it follows that (P',N') is the partition induced by (M'',M''), and since and is flat, is equivalent to , therefore and, by Lemma 4.6, . On the other hand, since , by Lemma 4.17 it follows that . Contradiction. Hence, is valid in , consequently condition (c) of the algorithm holds.

Finally, since and , by Theorem 4.10 it follows that . Moreover, since , from Lemma 4.6 it follows that , consequently , hence the propositional formula is satisfiable. Therefore, conditions (a), (b), and (c) in the algorithm hold, which implies that Flat-Not-Entails( ) returns true.

Only-if-part. If Flat-Not-Entails( ) returns true, then there exists a partition (P,N) of for which conditions (a), (b), and (c) of the algorithm hold. Let . By Definition 4.8, (P,N) is the partition of induced by (M,M). Now, since is satisfiable, there exists an interpretation I such that and , hence by Lemma 4.6 , and by Theorem 4.10 , therefore we only have to show that (I,M) is an model for . So, let us suppose (I,M) is not an model for . Then, by Lemma 4.17 there exists such that is satisfied in M'. Now, condition (c) in the algorithm implies that is a consequence of in , therefore is satisfied by each interpretation in M', that is, , which contradicts the hypothesis . Consequently, (I,M) is an model for .

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 .

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. PA (NPA) 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 , and of the polynomial hierarchy are defined by P, and for , , and . In particular, the complexity class is the class of problems that are solved in polynomial time by a nondeterministic Turing machine that uses an NP-oracle, and is the class of problems that are complement of a problem in , while is the class of problems that are solved in polynomial time by a nondeterministic Turing machine that uses an -oracle, and is the class of problems that are complement of a problem in . It is generally assumed that the polynomial hierarchy does not collapse: hence, a problem in the class or is considered computationally easier than a -hard or -hard problem.

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

Lemma 5.1   Let and let . Then, the problem of deciding whether is -hard.

Proof. As shown by [5], entailment in is -complete. Therefore, by Proposition 2.5, for subjective (and hence for general) theories, entailment is -hard.

Then, we show that the entailment problem in propositional is complete with respect to the class .

Theorem 5.2   Let and let . Then, the problem of deciding whether is -complete.

Proof. Hardness with respect to follows from Lemma 5.1. As for membership in , we analyze the complexity of the algorithm -Not-Entails reported in Figure 1. In particular, observe that:

• given (P,N), the formula can be computed in polynomial time with respect to the size of P. Moreover, by Lemma 4.9 it follows that, since has size linear with respect to the size of , construction of the partition can be performed through a linear number (with respect to the size of ) of calls to an NP-oracle for propositional satisfiability. Therefore, condition (a) can be checked through a linear number (in the size of the input) of calls to an NP-oracle;
• since , the formula can be computed in time linear with respect to the size of using an NP-oracle. And since, given and (P,N), can be computed in polynomial time with respect to the size of the input, it follows that condition (b) can be computed through a linear number (in the size of the input) of calls to an NP-oracle;
• given a partition (P',N'), each of the conditions (c1), (c2) and (c3) (analogous to conditions (a) and (b)) can be checked in polynomial time, with respect to the size of , using an NP-oracle. Therefore, since the guess of the partition (P',N') of requires a nondeterministic choice, falsity of condition (c) can be decided in , which implies that verifying whether condition (c) holds can be decided in .

Since the guess of the partition (P,N) of requires a nondeterministic choice, it follows that the algorithm -Not-Entails, if considered as a nondeterministic procedure, decides in nondeterministic polynomial time (with respect to the size of ), using a -oracle. Thus, we obtain an upper bound of for the non-entailment problem, which implies that entailment in is in .

The previous analysis also allows for a computational characterization of the logic [21], which is a slight modification of . Indeed, it is known [22] that, for each theory , M is an model of iff, for each interpretation I, (I,M) is an model of the subjective theory . Therefore, from Proposition 2.5 and from -hardness of entailment in [5], it follows that entailment in is -hard. Then, since iff [22], it follows that entailment in can be polynomially reduced to entailment in , hence such a problem belongs to . Therefore, the following property holds.

Theorem 5.3   Entailment in propositional is -complete.

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 . Therefore, skeptical entailment in GK is -complete.

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

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

Proposition 5.4   Let and let . Then, the problem of deciding whether is -complete.

As for complexity of entailment of generic queries with respect to flat 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 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 requires a nondeterministic choice, it follows that the algorithm runs in . Therefore, the following property holds.

Theorem 5.5   Let and let . Then, the problem of deciding whether is -complete.

Proof. Membership of the problem to the class is implied by the algorithm Flat-not-entails, whereas -hardness is implied by Proposition 5.4.

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 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 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 -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 . The main results presented can be summarized as follows:

• the negation as failure modality of exactly corresponds to negative introspection in . This implies that the logic can be viewed as the conservative extension of two different nonmonotonic modal logics: Halpern and Moses' logic of minimal knowledge and Moore's ;
• reasoning in the propositional fragment of lies at the third level of the polynomial hierarchy, hence (unless the polynomial hierarchy does not collapse) reasoning in is harder than reasoning in the best known propositional nonmonotonic logics, like default logic, autoepistemic logic, and circumscription;
• we have defined methods for reasoning in , which subsume and generalize well-known nonmonotonic reasoning algorithms used in logic programming [11], default logic [12], and autoepistemic logic [25];
• we have studied the flat fragment of and its relationship with the logic programming paradigm.

As for the computational aspects of reasoning in , 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 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 to be a tractable fragment of propositional logic, then the complexity of reasoning in the modal language built upon is lower than in the general case. In particular, it is easy to see that, under the assumption that entailment in can be computed in polynomial time, the algorithm -Not-Entails provides an upper bound of for -entailment in the fragment .

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.

## Bibliography

1
A. Beringer and T. Schaub.
Minimal belief and negation as failure: a feasible approach.
In Proc. of the 11th Nat. Conf. on Artificial Intelligence (AAAI'93), pages 400-405, 1993.

2
A. Bochman.
On bimodal nonmonotonic modal logics and their unimodal and nonmodal equivalents.
In Proc. of the 14th Int. Joint Conf. on Artificial Intelligence (IJCAI'95), pages 1518-1524, 1995.

3
J. Chen.
The logic of only knowing as a unified framework for non-monotonic reasoning.
Fundamenta Informaticae, 21:205-220, 1994.

4
F. M. Donini, D. Nardi, and R. Rosati.
Autoepistemic description logics.
In Proc. of the 15th Int. Joint Conf. on Artificial Intelligence (IJCAI'97), pages 136-141, 1997.

5
F. M. Donini, D. Nardi, and R. Rosati.
Ground nonmonotonic modal logics.
J. of Logic and Computation, 7(4):523-548, Aug. 1997.

6
T. Eiter and G. Gottlob.
Reasoning with parsimonious and moderately grounded expansions.
Fundamenta Informaticae, 17(1,2):31-54, 1992.

7
T. Eiter and G. Gottlob.
Propositional circumscription and extended closed world reasoning are -complete.
Theoretical Computer Science, 114:231-245, 1993.

8
T. Eiter and G. Gottlob.
On the computational cost of disjunctive logic programming: propositional case.
Annals of Mathematics and Artificial Intelligence, 15(3,4), 1995.

9
M. Gelfond and V. Lifschitz.
The stable model semantics for logic programming.
In Proceedings of the Fifth Logic Programming Symposium, pages 1070-1080. The MIT Press, 1988.

10
M. Gelfond and V. Lifschitz.
Logic programs with classical negation.
In Proceedings of the Seventh International Conference on Logic Programming, pages 579-597. The MIT Press, 1990.

11
M. Gelfond and V. Lifschitz.
Classical negation in logic programs and disjunctive databases.
New Generation Computing, 9:365-385, 1991.

12
G. Gottlob.
Complexity results for nonmonotonic logics.
J. of Logic and Computation, 2:397-425, 1992.

13
G. Gottlob.
NP trees and Carnap's modal logic.
J. of the ACM, 42(2):421-457, 1995.

14
J. Y. Halpern and Y. Moses.
Towards a theory of knowledge and ignorance: Preliminary report.
In K. Apt, editor, Logic and models of concurrent systems. Springer-Verlag, 1985.

15
J. Y. Halpern and Y. Moses.
A guide to completeness and complexity for modal logics of knowledge and belief.
Artificial Intelligence, 54:319-379, 1992.

16
K. Inoue and C. Sakama.
On positive occurrences of negation as failure.
In Proc. of the 4th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR'94), pages 293-304. Morgan Kaufmann, Los Altos, 1994.

17
T. Janhunen.
On the intertranslatability of autoepistemic, default and priority logics.
In Proc. of the 6th European Workshop on Logics in Artificial Intelligence (JELIA'98), pages 216-232, 1998.

18
D. S. Johnson.
A catalog of complexity classes.
In J. van Leuven, editor, Handbook of Theoretical Computer Science, volume A, chapter 2. Elsevier Science Publishers (North-Holland), Amsterdam, 1990.

19
M. Kaminski.
Embedding a default system into nonmonotonic logics.
Fundamenta Informaticae, 14:345-354, 1991.

20
H. J. Levesque.
All I know: a study in autoepistemic logic.
Artificial Intelligence, 42:263-310, 1990.

21
V. Lifschitz.
Nonmonotonic databases and epistemic queries.
In Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI'91), pages 381-386, 1991.

22
V. Lifschitz.
Minimal belief and negation as failure.
Artificial Intelligence, 70:53-72, 1994.

23
V. Lifschitz and T. Woo.
Answer sets in general nonmonotonic reasoning (preliminary report).
In Proc. of the 3rd Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR'92), pages 603-614. Morgan Kaufmann, Los Altos, 1992.

24
F. Lin and Y. Shoham.
Epistemic semantics for fixed-point non-monotonic logics.
Artificial Intelligence, 57:271-289, 1992.

25
W. Marek and M. Truszczynski.
Nonmonotonic Logics - Context-Dependent Reasoning.
Springer-Verlag, 1993.

26
W. Marek, M. Truszczynski, and A. Rajasekar.
Complexity of computing with extended propositional logic programs.
Annals of Mathematics and Artificial intelligence, 15(3,4), 1995.

27
R. C. Moore.
Semantical considerations on nonmonotonic logic.
Artificial Intelligence, 25:75-94, 1985.

28
I. Niemelä.
On the decidability and complexity of autoepistemic reasoning.
Fundamenta Informaticae, 17(1,2):117-156, 1992.

29
Computational Complexity.

30
R. Reiter.
What should a database know?
J. of Logic Programming, 14:127-153, 1990.

31
R. Rosati.
Reasoning with minimal belief and negation as failure: Algorithms and complexity.
In Proc. of the 14th Nat. Conf. on Artificial Intelligence (AAAI'97), pages 430-435. AAAI Press/The MIT Press, 1997.

32
R. Rosati.
Reasoning about minimal knowledge in nonmonotonic modal logics.
J. of Logic, Language and Information, 8(2):187-203, 1999.

33
G. Schwarz.
Autoepistemic logic of knowledge.
In Proc. of the 1st Int. Workshop on Logic Programming and Non-monotonic Reasoning (LPNMR'91), pages 260-274. The MIT Press, 1991.

34
G. Schwarz.
Minimal model semantics for nonmonotonic modal logics.
In Proc. of the 7th IEEE Sym. on Logic in Computer Science (LICS'92), pages 34-43. IEEE Computer Society Press, 1992.

35
G. Schwarz.
On embedding default logic into Moore's autoepistemic logic.
Artificial Intelligence, 80:388-392, 1996.

36
G. Schwarz and V. Lifschitz.
Extended logic programs as autoepistemic theories.
In Proc. of the 2nd Int. Workshop on Logic Programming and Non-monotonic Reasoning (LPNMR'93), pages 101-114. The MIT Press, 1993.

37
G. Schwarz and M. Truszczynski.
Minimal knowledge problem: a new approach.
Artificial Intelligence, 67:113-141, 1994.

38
Y. Shoham.
Nonmonotonic logics: Meaning and utility.
In Proc. of the 10th Int. Joint Conf. on Artificial Intelligence (IJCAI'87), pages 388-392, 1987.

39
R. Stalnaker.
A note on non-monotonic modal logic.
Artificial Intelligence, 64(2):183-196, 1993.

#### Footnotes

...,1
We denote as B the modal operator used in .

1999-10-09