On Bimodal Nonmonotonic Logics and Their Unimodal and Nonmodal Equivalents

Introduction

In many respects, the logic of belief and negation as fail­ ure (MBNF) suggested in [1ifschitz, 1994] can be seen as a most general formalism for nonmonotonic reasoning that provides a unifying framework both for logic pro­ gramming and for such nonmonotonic systems as default and autoepistemic logic. In this paper we consider the relation of MBNF to other nonmonotonic formalisms. Our main results are twofold. On the one hand, MBNF is shown to be reducible to usual unimodal nonmono­ tonic logics. On the other hand, we also show that it can be reduced to nonmodal default consequence rela­ tions from [Bochman, 1993; 1994] .

The paper is organized as follows. We show first that MBNF is equivalent to a certain nonmodal system, called a BNF -consequence relation, that involves rules, or se­ quents, of a speci:1l kind. In this framework we define a counterpart of 1ifschitz models and the notion of an L-expansion that can be cor. .idered as their 'core'. In addition, we introduce the notion o: ::..n 1-extension that also turns out to correspond to weH-known objects from other nonmonotonic formalisms. Next, we show that BNF-consequence relations admit a modal representa­ tion that uses only one modal operator, the operator of belief. Moreover, under this translation, 1-expansions correspond to §-expansions (in the sense of [Marek et al., 1993]) of the associated modal nonmonotonic logic. Finally, we show that, as far as 1ifschitz models are con­ cerned, MBNF is reducible to nonmodal default conse­ quence relations from [Bochman, 1994].

These results have important implications for a gen­ eral theory of nonmonotonic reasoning. They show, in effect, that many apparently different nonmonotonic formalisms are actually different representations of the same basic constructions and reasoning principles .

1 MBNF and its reductions

The language of MBNF involves two independent modal operators, B for belief and not for negation as fail­ ure. As the majority of nonmonotonic systems , MBNF involves two components. One is a (monotonic) host logical system, the other is the notion of a model that generates the corresponding nonmonotonic infer­ ence. The system is characterized semantically: MBNF­ interpretations are triples of the form (I, Sb, sn) , where I is an ordinary interpretation (a set of atomic proposi­ tions) and Sb, sn are sets of such interpretations. Such triples are used to define the notion of truth as follows :

• (i) IfF is an atom, F is true in (I,Sb ,Sn) iff FE I.
• (ii) -.F is true in (I ,Sb,Sn) iff F is not true in (I, sb, sn) .
• (iii) F 1\ G is true in (I, Sb, sn) iff F and G are both true in (I, sb, sn ).
• (iv) BF is true in (I, Sb, sn) iff, for all J E Sb, F is true in ( J, sb, sn).
• ( v) not F is true in (I , Sb, sn) iff, for some J E sn, F is not true in ( J, sb, sn).

Note that there is nothing nonmonotonic in the above conditions; they can be seen as a semantic description of the host monotonic logical system for MBNF . The nonmonotonic component of MBNF is embodied in the notion of a model. A model of a theory T is defined by 1ifschitz as a pair (I, S) such that Tis true in (I, S, S) and there are no J, S' such that S' properly includes S and T is true in ( J, S', S). This notion of a model gives rise to a corresponding notion of entailment, which is already nonmonotonic.

To begin with, note that the semantic characteriza­ tion of MBNF gives rise to natural monotonic notions of semantic entailment and equivalence. Thus, we will say that a set of propositions u semantically entails a propo­ sition A if A is true in all MBNF-interpretations in which u is true. Similarly, two sets of propositions u and v will be called semantically equivalent if they are true in the same MBNF-interpretations. These notions of entail­ ment and equivalence are stronger than similar notions defined in [Lifschitz, 1994], because they are defined in terms of all interpretations 1 . It should be clear , how­ ever , that sets of propositions that are equivalent in our sense are interchangeable in all contexts and construc­ tions that are definable on the basis of MBNF-semantics , including, in particular, Lifschitz models.

Now, an important feature of MBNF is that any for­ mula turns out to be strongly equivalent to a formula without nested occurrences of the modal operators (we will call such formulas fiat ones), and the correspond­ ing reduction can be accomplished using a simple and efficient procedure. Moreover , we have

Proposition 1.1 Any set of MBNF-formulas is seman­ tically equivalent to a set of fiat MBNF-clauses

An objective representation of MBNF, described be­ low, is based on an identification of the above flat clauses with rules of the form alb : cld If- A, where a, b, c, d are finite sets of objective propositions. To be more exact, a clause of the above form can be identified with a rule

We will call such rules BNF-sequents. Thus, a sequent alb : cld If- A corresponds to a rule saying that if propo­ sitions from a are believed, propositions from b are not believed, propositions from c are not rejected by failure and propositions from d are rejected by failure, then we can infer that A is true. The following definition gives a characterization of such sequents corresponding to flat MBNF-clauses. f- below denotes the ordinary classical consequence, ..L the proposition 'false'.

Definition 1.1 A BNF-consequence relation is a set of BNF-sequents satisfying the following conditions:

( B-Factoring)

1 Still, these stronger notions are implicit in [Lifschitz, 1994] in the form of the first-order entailment and equiv­ alence between nonmodal reductions of MBNF-formulas ob­ tained by replacing the two modal operators with quantifiers.

Despite the number of conditions, BNF-consequence relation is a conceptually simple system. Note first that the above definition can be easily extended to infinite premise sets using the following compactness require­ ment : for any sets of propositions u, v, w and x ,

for some finite a, b, c, d such that a ~ u , b ~ v , c ~ w and de x.

In ~hat follows , we will denote by Cn the (four­ argument) provability operator corresponding to If-. Let u denote the complement of a set u. Now, BNF­ consequence relations can be characterized in terms of the following notion of a model.

Definition 1.2 A triple ( i, u, v) of sets of propositions will be called a model of If- if i is a maximal consistent set (a 'world') and Cn(ulu: vlv) ~ i .

Note that i is a deductively closed set . Moreover , (B-Closure) and (N-Closure) imply that if (i, u, v) is a model, then u and v must also be deductively closed sets. The following representation theorem gives a char­ acterization of BNF-consequence relations in terms of their models:

Theorem 1.2 alb : cld If- A iff A E i , for any model ( i, u, v) such that a ~ u, b ~ u, c ~ v and d ~ v .

It is easy to see that any set of triples ( i , u , v) of de­ ductively closed sets generates a BNF -consequence rela­ tion in accordance with the above representation. Note also that models in our sense can be seen as syntactic counterparts of MBNF-interpretations: instead of sets of worlds, our models include sets of propositions that are true in them. In view of this fact , the above theorem can be used to show the correspondence between MBNF theories and BNF-consequence relations.

Recall that any MBNF theory Tis semantically equiv­ alent to some set T1 of flat MBNF -clauses. Let lf-T de­ note the least BNF -consequence relation containing all sequents corresponding to clauses from T1, and let Fs denote a flat MBNF -clause corresponding to a BNF­ sequent s. The following theorem shows that lf-T is ade­ quate for representing the 'flat content' ofT.

Theorem 1.3 s E lf-T iff T entails F, .

Given the correspondence between models and MBNF-interpretations, the following corollary is an im­ mediate consequence of the theorem.

Corollary 1.4 Models of lf-r exactly correspond to MBNF-interpretations satisfying T.

Thus, for any MBNF theory there is a BNF­ consequence relation that is in a strong sense equiva­ lent to it. It is important to note that this correspon­ dence between MBNF theories and BNF-consequence re­ lations does not depend on the nonmonotonic component of MBNF, namely on Lifschitz notion of a model. In the next section we will consider such models in detail.

2 Lifschitz models

The following definition provides a characterization of Lifschitz models (or, in short, L-models) in the frame­ work of BNF-consequence relations .

Definition 2.1 A pair (i, u) will be called an L-model of If- if (i, u , u) is a model and there is no model (j, u', u) such that u' C u.

By Corollary 1.4, this definition is adequate, since Lif­ schitz models of a theory T correspond to L-models of lf-r . We consider now reformulations of the definition that would display the 'internal structure' of L-models.

A pair ( u, v) of sets of propositions will be called a bitheory in If- if ulu: vlv W L Clearly, ( u, v) is a bitheory if and only if there is a world i such that ( i, u, v) is a model.

A bitheory ( u, v) will be called B-minimal if there is no bitheory (u', v) such that u' C u. Now, it is easy to show that (i, u) is an L-model if and only if

• (i) Cn(ulu : ulu) ~ i ;
• (ii) (u,u) is a B-minimal bitheory.

For reasons that will become clear later , a set u will be called an L- expansion if (u, u) is a B-minimal bithe­ ory. Thus, any L-model is a pair consisting of an L­ expansion u and a maximal deductively closed set con­ taining Cn ( u lu : u lu) . It is interesting to note that L­ expansions correspond to what was termed models in MKNF, a freliminary version of MBNF given in [Lifs­ chitz, 1991 (see below). In addition, L-expansions cor­ respond also to preferred models of the bimodal logic GK suggested in [Lin and Shoham, 1992].

Remark. It is easy to show that GK and MBNF are equivalent (modulo notational variants) for flat modal theories. Moreover, as is noted in [Lin and Shoham, 1992], flat formulas are sufficient for determining the no­ tion of a preferred model of GK. Thus, as far as intended models are concerned, the two systems can be seen as equivalent.

Now we consider some additional rules and conditions that can be imposed on BNF -consequence relations. The following rules are of a special interest:

(Nontriviality) requires our beliefs to be consistent, (L-Coherence) says that believed propositions cannot be negated by failure, while (G-Coherence) is a partial in­ verse of (L-Coherence); it says that if assuming that some propositions are negated by failure and some are not imply that a certain set of beliefs is inconsistent, then one of the propositions from this set can be negated by failure provided the rest of these propositions is believed.

A BNF -consequence relation will be called nontriv­ ial if it satisfies (Nontriviality) , coherent if it satis­ fies (L-Coherence) and strongly coherent if it satisfies both (L-Coherence) and (G-Coherence) . Let Ire be the least strongly coherent consequence relation containing If- . Clearly, it is a consequence relation obtained from If­ by simply adding the relevant rules. The following result shows that these rules preserve L-models.

Proposition 2.1 Ire has the same L-modds as If-.

As to (Nontriviality), it can be shown to preserve L­ models with consistent L-expansions.

For coherent BNF-consequence relations, the condi­ tions for L-models can be simplified.

Proposition 2.2 For any coherent BNF-c.r.:

(i) A consistent set u is an L-expansion if and only if

(ii) ( i , u) is an L-model iff u is an L- expansion and i is a maximal consistent set that includes Cn(010 : ulu).

To conclude this section, we define still another non­ monotonic object that will play an important role in what follows. A bitheory (u, v) will be called minimal if there is no other bitheory ( u', v') such that u' ~ u and v' ~ v. Now, a set u will be called an L- extension of If­ if (u, u) is a minimal bitheory.

Clearly, any 1-extension is an 1-expansion. However, the former notion is stronger; it embodies both the re­ quirement of minimality of beliefs and the principle of maximality of negation as failure assignments 2 . As we will see, such objects correspond to well known con­ structs in other nonmonotonic formalisms . The following proposition gives a characterization of L-extensions for coherent consequence relations:

Proposition 2.3 A consistent set u is an L- extension of a coherent BNF- c. r. If- iff u ={A I lA : lu If- 1_} .

3 A unimodal re-presentation

In this section we are going to show that coherent BNF­ consequence relations admit, in turn, a modal represen­ tation that involves only one modal operator , B . It is obtained by identifying 'not' with B·B 3 . To be more exact, a sequent s of the form

is representable by the following formula that we will denote by s:

2 0r the requirement of minimality of assumptions, in the terminology of [Lin and Shoham, 1992].

3 T his identification was also used in [Lifschitz and Schwarz, 1993], though for a restricted class of theories.

In the literature on modal logics one can meet two commonly used notions of modal consequence that re­ flect two main notions of validity of propositions with re­ spect to possible world models. Let §be a normal modal logic. A proposition A is called a local §-consequence of a set of propositions u (notation u f-~ A) if A is provable from u and theorems of § using modus ponens only; A is called a global §-consequence of u (notation u f-~ A), if A is provable from u and theorems of § using modus ponens and the necessitation rule A/LA. In this study we will extensively use both these notions.

Theorem 3.1 Let If- s be the least nontrivial coherent consequence relation containing a set of sequents S and S the set of unimodal formulas corresponding to sequents from S . Then a sequent s belongs to lf-s iff Sf-~ s, for any normal modal logic§ between KD4G and KD4I.

Here KD4G denotes a modal logic corresponding to Kripke frames with transitive and directional accessibil­ ity relations (see [Bull and Segerberg, 1984]), while KD4I is a logic introduced in [Bochman, 1994]; it is determined by directional Kripke frames of depth :::; 3.

The theorem shows that the above unimodal transla­ tion is adequate for a representation of coherent BNF­ consequence relations. Consequently, it is adequate for capturing the nonmonotonic MBNF-inference based on Lifschitz models. Note, however, that the translation itself does not depend on L-models and is adequate for any notion definable in terms of (coherent) BNF­ consequence relations. For example, using the results from [Bochman, 1993], sets u satisfying the condition ICns(ulu: 010) ~ u can be shown to correspond to ob­ jective subsets of stable sets containing S, while sets sat­ isfying u = Cns(ulu: 010) correspond to Moore's stable expansions of S.

Remark. Using the above results, we can perform a two-step translation of MBNF-formulas into unimodal ones: we first reduce an MBNF-formula to a flat one and then replace all occurrences of 'not' in it by B·B. Note, however, that this procedure cannot be short­ ened to a direct replacement of 'not' in MBNF-formulas, since the above unimodal translation does not account for the interaction between nested modal operators of MBNF. Consequently it is inadequate if applied to non­ flat MBNF-formulas.

Thus , we have shown, in effect, that MBNF can be returned to the family of usual modal nonmonotonic logics . In the next section we will complete the pic­ ture by demonstrating that, under this reformulation, L-expansions correspond to modal §-expansions in the sense of [Marek et al., 1993].

4 Biconsequence relations and L-expansions

BNF-sequents of the form alb : cld If- ..l will be called 1..-sequents. Such sequents correspond to modalized MBNF-formulas in which any propositional atom occurs in the scope of some modal operator . Note that all cur­ rent applications of MBNF (see, e.g., [Inoue and Sakama,

1994; Lifschitz and Woo, 1992; Lifschitz and Schwarz, 1993]) use only formulas of this kind.

Let us rewrite .1.-sequents as rules of a new kind as follows: a sequent alb : cld If- ..l will correspond to a rule

We will call these rules bisequents. Such rules can be seen as representing entailment relations between pairs of sets of propositions. In accordance with the original interpretation of BNF-sequents, bisequents can be read as follows: "If all propositions from a are believed and all propositions from d are negated by failure, then either one of the propositions from b should be believed or one of the propositions from c should be negated by failure". This interpretation also justifies the particular order of the four parameters chosen for representing the rules.

Definition 4.1 A set of bisequents will be called a bi­ consequence relation if it satisfies the following condi­ tions and rules:

It is easy to see that the above conditions are sim­ ply reformulations of the corresponding conditions for BNF-consequence relations. Note that, by Theorem 1.2, ..l-sequents are determined by bitheories only. Accord­ ingly, models of a biconsequence relation can be defined as pairs ( u, v) such that u : v .IlL u: v . Then we have

Theorem 4.1 If If- is a biconsequence relation, then a: b If- c: d iff, for any model (u,v), if a~ u and b ~ v, then either c n u f. 0 or d n v f. 0.

Clearly, any BNF-consequence relation contains a hi­ consequence sub-relation that is determined by its bithe­ ories. Moreover, these biconsequence subrelations can be shown to be conservative in the sense that they prove all and only ..l-sequents that are provable in the correspond­ ing BNF-consequence relation.

Instead of L-models, we now have only L-expansions defined as sets u such that ( u, u) is a B-minimal model , while L-extensions are defined as minimal models. Then it is easy to see that L-expansions and L-extensions of a BNF -consequence relation coincide with the correspond­ ing objects of the associated biconsequence relation.

The conditions of coherence, strong coherence and nontriviality can be immediately transferred to bicon­ sequence relations (since they are formulated in terms of ..l-sequents); as before, they will preserve L-expansions. Moreover, in this case the latter can be characterized as sets satisfying

while 1-extensions will be characterized by

The correspondence between BNF- and biconsequence relations implies that bisequents admit the same uni­ modal representation as l_-sequents. Moreover, it can be shown that in this case a local modal consequence determined by any modal logic in an extended range KD4G- S4F would be appropriate for nontrivial coher­ ent biconsequence relations.

The next theorem shows that a global modal conse­ quence is adequate for representing strongly coherent hi­ consequence relations.

Theorem 4.2 A sequent s belongs to the least nontrivial strongly coherent biconsequence relation containing S if and only if S 1-~ s, for any normal modal logic§ between KD4G and S4F.

The main result of this section is that under the uni­ modal translation 1-expansions correspond to modal §­ expansions in the sense of [Marek et al., 1993]. St(u) below denotes the unique modal stable set having u as its objective subset.

Theorem 4.3 /fll-} is the least strongly coherent bicon­ sequence relation containing a set of bisequents S, then, for any normal modal logic § in the range S4.2-S4F,

• (i) A consistent set u is an L-expansion in II-} iff St(u) is an § -expansion of S.
• (ii} A consistent set u is an L-extension in II-~ iff St(u) is a ground § -expansion of§.

Thus, 1-expansions are representable as objective sub­ sets of modal expansions, while 1-extensions correspond in this sense to ground expansions. Another important fact that can be obtained from the proof of this theorem is th<'t this correspondence between biconsequence rela­ tions and modal nonmonotonic logics is reversible in the sense that , for any modal theory T and any modal logic in the above range, §-expansions of T are representable as 1-expansions of some biconsequence relation.

4.1 A note on MKNF

An earlier version of MBNF was presented by Lifschitz in [Lifschitz, 1991] . The system was called MKNF, be­ cause its first modal operator was termed an operator of knowledge. Though it involved the same semantic inter­ pretation, the definition of a model was different. With­ out going into details here, it can be shown that these models are exactly 1-expansions of BNF -consequence re­ lations satisfying the following additional rule:

In the context of MBNF, the rule means that provable conclusions should be believed. In fact, the rule reme­ dies one of the puzzling features of MBNF, namely that propositions provable on the basis of some set of beliefs, non-beliefs and negations by failure have, in turn, almost no impact on our beliefs or on what could be negated by failure . In this sense, MBNF is not a system of intro­ spective reasoning.

Another possible constraint that follows from the in­ formal interpretation of the first modal operator as an operator of knowledge is the following condition saying, in effect, that knowledge implies truth:

However, adding this condition would make any BNF­ sequent equivalent to some 1_-sequent:

Proposition 4.4 A BNF-consequence relation satisfies (Cut) and (Reflexivity) if and only if

As a result, MKNF would be reducible to biconse­ quence relations.

5 Default consequence relations

By Proposition 2.2, the two components of an 1-model are determined, in effect, by different subsystems of co­ herent BNF-consequence relations: 1-expansions are de­ termined by sequents of the form lA : alb II- l_ , while world components are determined by sequents of the form I : alb II- A. In both cases we seek for conse­ quences of negation as failure assignments: belief propo­ sitions that follow from such assignments characterize L-expansions, while objective consequences determine world components of L-models. Now, it turns out that both kinds of sequents generate default consequence re­ lations in the sense of [Bochman, 1994].

Default consequence relations were defined in [Bochman, 1994] as consequence relations involving se­ quents of the form a : b II- A. Such sequents can be seen as special cases of BNF-sequents. Note, however , that there is actually a number of possibilities for 'embedding' default sequents into BNF-sequents, and in this way dif­ ferent default consequence relations can be obtained.

A most interesting default consequence relation for our present study can be defined as follows:

When II- is coherent, this default consequence rela­ tion satisfies all the properties of an autoepistemic con­ s~quence relation as defined in [Bochman, 1994]. The latter has been shown to be adequate for representing autoepistemic logic ([Moore, 1985]), where Moore's sta­ ble expansions are representable as sets satisfying the condition u = Cn( u : u) . Such sets were termed expan­ sions of the corresponding default consequence relation. Now, the following theorem shows that expansions of 11-a are exactly L-expansions of II- .

Theorem 5.1 If II- is a coherent BNF-consequence re­ lation, then 1-a is an autoepistemic consequence relation. Moreover, consistent expansions ofl-a coincide with con­ sistent L-expansions of II-.

The theorem can be seen as a generalization of Theo­ rem 4.4 from [Lin and Shoham, 1992] giving a represen­ tation of autoepistemic logic in GK.

Another interesting default consequence relation arises when we treat BNF-sequents of the form alA: lb II- l_ as representing default sequents:

Such an interpretation corresponds, in fact, to that used in [Lifschitz , 1994; Lin and Shoham, 1992] for rep­ resenting default logic. If If- is strongly coherent, lf-r is what is called in [Bachman, 1994] a reflexive default con­ sequence relation. The latter has been shown to be ade­ quate for representing default logic [Reiter, 1980], where extensions correspond to sets satisfying the condition u = Cn(0 : u). Now we have

Theorem 5.2 If Ifis a strongly coherent BNF­ consequence relation, then lf-r is a reflexive default con­ sequence relation. Moreover, consistent extensions of lf-r coincide with L-extensions of If-.

The reader may notice an apparent discrepancy be­ tween the above two representation results, especially if compared with the relevant results from [Lifschitz, 1994; Lin and Shoham, 1992], where extensions were actually shown to correspond to 1-expansions, as well as with the results from [Truszczynski , 1991a; 1991b] about em­ bedding of default logic into modal nonmonotonic log­ ics where extensions were shown to correspond to §­ ex~ansions4. This discrepancy reveals an important, though subtle, general point about the correspondence between existing nonmonotonic formalisms .

The above mentioned results may create an impres­ sion of a broad equivalence between the relevant objects from different nonmonotonic formalisms . This impres­ sion can even be strengthened with Theorem 4.3(i) above that establishes a correspondence between 1-expansions in MBNF and §-expansions in modal nonmonotonic log­ ics as well as with the result from [Bachman, 1994] sa;ing that §-expansions can be characterized precisely , as extensions of modal default consequence relations. ' Still, the impression is slightly misleading. In fact, as far as only objective propositions are concerned, there are two kinds of nonmonotonic objects here . One kind includes 1-expansions of MBNF and objective kernels of §-expansions of modal nonmonotonic logics. The other more specific kind includes extensions of de­ fault logic , objective ~ubsets of ground §-expansions and 1-extensions ( cf. Theorem 4.3 above and [Bachman, 1993]) . The difference between these two kinds of ob­ jects can be easily demonstrated if we notice, for exam­ ple, that an 1-expansion can be a subset of another 1expansion, which is impossible, e.g., for (L-)extensions.

The following general result (cf. also [Lifschitz and Woo , 1992]) shows that the distinction is due to the pres­ ence of positive occurences of 'not' in MBNF-formulas.

Theorem 5.3 Let lf-s the least BNF-consequence rela­ tion containing a set S of BNF-sequents of the form alb : ld If- A . Then any L-expansion of lf-s is an L­ extension.

This result implies, in particular, that Truszczynski's translation of default theories generates only modal the­ ories all expansions of which are ground. Such a trans­ lation is not reversible-objective subsets of expansions are not representable, in general, as extensions of some default theory.

4 Note that the translation used by Truszczynski is actually a special case of the unimodal translation given above.

Finally, note that the following definition:

also determines a default consequence relation. This consequence relation involves BNF-sequents that are 're­ sponsible' for world components of 1-models in the sens.e that , if u is an 1-expansion, then (i, u) is an L-model1f and only if Cne(u: u) ~ i.

Thus the main conclusion that can be made from the above ;esults is that default consequence relations are sufficiently expressive to capture the major nonmono­ tonic objects of MBNF. In this sense MBNF is reducible to the former .

6 Conclusions

This study can be seen as a contribution to a (future) general theory of nonmonotonic reasoning. Correspon­ dencies established between logic programming, default logic and various modal nonmonotonic logics, including those stated above, strongly indicate that all these for­ malisms give rise to essentially the same nonmonotonic constructions. Moreover, our results show that the corre­ spondence between these formalisms can be extended to the level of underlying reasoning systems and hence does not depend on particular nonmonotonic objects chosen.

Among other nonmonotonic systems, MBNF is clearly one of the most expressive formalisms. Moreover , as we have seen, it is even too powerful in its expressive capa­ bilities for the objects considered as its intended models. However the list of plausible nonmonotonic objects is by no m~ans closed, and there are indications that this framework or its fragments (such as biconsequence rela­ tions introduced above), could be appropriate for many of them. However, this is a subject for another study.

Acknowledgments

The author is grateful to Vladimir Lifschitz for his help­ ful advices on an earlier version of the paper.