Riccardo Rosati
Dipartimento di Informatica e Sistemistica
Università di Roma ``La Sapienza''
Via Salaria 113, 00198 Roma, Italy
email: rosati@dis.uniroma1.it
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].
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,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 structure is defined inductively as follows:
We write to indicate that is satisfied by (I,M_{b},M_{n}). We say that a theory is satisfied by (I,M_{b},M_{n}) (and write ) iff each formula from is satisfied by (I,M_{b},M_{n}). 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 M_{n}, and we also write . If then the evaluation of does not depend on the sets M_{b},M_{n}, 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 M_{b}, M_{n} 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.
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 .
Given a set of interpretations M, Th(M) denotes the set of formulas such that and . Let M_{1},M_{2} be sets of interpretations. We say that M_{1} is equivalent to M_{2} iff Th(M_{1})=Th(M_{2}).
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.
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,M_{1}), where M_{1} corresponds to the set of all interpretations (which represents the case in which is not assumed to hold); and (J,M_{2}), 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 .
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 .
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].
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 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.
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:
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.
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 .
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 ).
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.
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.
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. .
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.
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.
In order to simplify notation, we denote as the partition . The following theorem provides a constructive way to build the partition .
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 .
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].
Proof. Let : from the above definition and Definition 3.2, it follows immediately that . Therefore, if then iff .
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.
Suppose now that
(P,N)=(P_{2},N_{2}), where
To prove correctness of the algorithm -Not-Entails we need the following preliminary lemma.
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.
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].
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, P_{n} 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 ,^{1}since 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.
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.
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.
Based on the above property, we are now able to prove correctness of the algorithm Flat-Not-Entails.
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].
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. 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 , 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.
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 .
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:
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.
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.
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.
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.
In this paper we have investigated the problem of reasoning in the propositional fragment of . The main results presented can be summarized as follows:
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].
This research has been partially supported by Consiglio Nazionale delle Ricerche, grant 203.15.10.