The Power of Beliefs or Translating Default Logic into Standard Autoepistemic Logic

1 Introduction

Reiter's default logic [16] and Moore's autoepistemic lo­ gic [14] are among the most relevant formalizations of nonmonotonic logic. A first investigation into the re­ lationship between default and autoepistemic logic was carried out by Konolige [8] .

Konolige [8] encountered some groundedness-problems in Moore's original version of autoepistemic logic (stan­ dard AEL), which impeded a straightforward tr_ansla­ tion of default logic into standard AEL. In particular, the autoepistemic theory A that would most intuitively correspond to a given default theory T in many cases ad­ mits some additional stable expansions that do not cor­ respond to any default extensions ofT. These additional expansions are weakly grounded in the initial pr~mise~ in the sense that they contain sentences p whose mcluswn is merely based on the agent's belief in p. Consequently, Konolige has defined a more restrictive version of au­ toepistemic logic that we will here call strongly groun­ ded autoepistemic logic (SGAEL) . In SGAEL, only specific strongly grounded expansions are admissible. Each strongly grounded expansion is a stable expansion in the sense of standard AEL, but not vice-versa. Konolige succeeds in showing that SGAEL exactly corresponds to default logic and exhibits bidirectional translations bet­ ween these two formalisms [8].

·This is a short version of the full paper (4] available from the author by email/ftp.

SGAEL differs significantly from standard AEL. In particular, in SGAEL it may be the case that two lo­ gically equivalent but syntactically differe~t s~ts of rre­ mises E1 and E2 have a. different semantics, 1.e., diffe­ rent respective sets of SGAEL-expansions. Further, all strongly grounded extensions of a theory E are stable-set minimal for E, which is not the case in standard AEL.

The second major approach of translating default logic into variants of AEL has been taken by Marek, Schwarz, and Truszczynski [12; 20; 19]. Their approach is based on the concept of nonmonotonic modal logics as introdu­ ced by McDermott [13]. They show that default logic is faithfully embeddable in a wide range of differen~ n~nmo­ notonic modal logics. The simplest of these log1cs IS the nonmonotonic counterpart of the pure logic of necessita­ tion N - the modal logic consisting of propositional cai­ culus augmented by the necessitation rule. We will make intensive use of this logic in the present paper. Note that just as SGAEL, nonmonotonic N is considered a ~tron­ ger logic than standard AEL, since each N-expans~on of a set of premises E is also a standard AEL-expans1on of E, but not vice-versa.

In [17] it is shown that standard AEL corresponds to the nonmonotonic version of the modal logic KD45 ba­ sed on the modal axioms K , 4, 5, and D : L<P - -,L-,¢1. Unfortunately, the proposed translations schemes which allow the embedding of default logic into a large num­ ber of other nonmonotonic modal logics fail to apply to nonmonotonic KD45, hence they are not applicable to standard AEL.

Other methods for translating default logic into forma­ lisms close to AEL have been developed by Niemela [15], Lin and Shoham [9], Siegel [18], and Kaminski [7] . E~ch approach introduces a different version ?f ~EL wh1ch captures default logic. Each of these log1cs IS more re­ strictive than standard AEL in the sense that, in general, a set E of given premises in these logics admits fewer ex­ pansions than in standard AEL.

In summary, all previous methods translate default logic into formalisms that are different from standard AEL. The reason seems to be that standard AEL allows for expansions that are not sufficiently grounded in the premises. Consequently, these approaches are based on more restrictive formalisms that admit less expansions .

The question whether default logic can be translated into standard AEL has remained open so far . In the present paper, we solve this problem by giving both a negative and a positive answer.

First (in Section 2), we show that there exists no mo­ dular translation between default logic and AEL. This means that after adding a new fact F to the formula set W of a default theory (D, W}, a complete recomputation of the translation becomes necessary. An exception are prerequisite-free default theories, which are modularly translatable to standard AEL.

In Section 3, we show that it is possible to polynomi­ ally translate general default theories to standard AEL if one gives up on modularity. Section 4 concludes the paper with a philosophical interpretation of our transla­ tion.

In this paper we limit ourselves to consider proposi­ tional default logic and AEL. Note that the impossibi­ lity result for modular translations extends trivially from propositional default logic to the more general first order case. We assume that the reader is familiar with default logic and AEL and do not redefine these concepts.

2 Impossibility of Modular Translation

Let us first define the concept of faithful translation .

Definition 2.1 A faithful translation from default lo­ gic to AEL is a mapping tr which transforms each de­ fault theory V into an autoepistemic theory tr(V) such that the objective parts of the autoepistemic expansions of tr(V) are identical with the default extensions of V .

The concept of modular translation in the context of default logic was introduced by Tomasz Imielinski in [6] . Loosely speaking, a translation scheme is modular if ad­ ding new facts (not defaults) to a default theory is re­ flected by the translation through adding these new facts to the result of the translation. Imielinski [6] considered translations between default logic and circumscription. We adapt his formal definition of modularity to the con­ text where AEL is the target system as follows .

Definition 2.2 A translation tr from default logic to AEL is modular iff for each default set D and each W ~Cit holds that tr((D, W)) = tr((D,0)) U W.

As Imielinski points out, modular translations are highly desirable both from the conceptual and the com­ putational point of view. Indeed, changes to a default theory (D, W), due to changes in the underlying "real world", will in most cases affect W but not D, as the de­ fault rules in D usually represent time-invariant proper­ ties. With a modular translation, when W is changed, we do not have to recompute the result of the transla­ tion, but we may just add the new elements of W to the old result.

Note that both Konolige's translation from default lo­ gic to SGAEL [8] and Truszczynski's translation T from default logic to nonmonotonic N are modular. In the rest of this section, we will show that a faithful modu­ lar translation from default logic to standard AEL is not possible. In particular, such a translation is not possible even if the defaults are restricted to very simple classes such as normal defaults. We will, however, identify one important class of defaults admitting a faithful modular translation to standard AEL, namely the prerequisite­ free defaults.

Theorem 2.1 There exist no faithful modular transla­ tion from default logic into standard AEL. Such a trans­ lation does not exist even if the defaults are restricted to be normal.

PROOF. Consider the normal default (D, Wo), (D, W1), and (D, W2), where Wo {a}, w2 ={a-+ b}, and theories 0, w1 =

Each of these three default theories has exactly one ex­ tension. (D, W0 ) has as unique extension cons(0), while (D, W1) and (D, W2) both have the set cons( {a, b}) as unique extension. Here cons(X) denotes {¢>IX f= ¢>} .

Assume that there exists a modular faithful transla­ tion tr from default logic to standard AEL. We will show that this assumption implies that cons( {a, b}) is an ex­ tension of (D, W0 ), an obvious contradiction.

Let tr((D,W0)) = ~ - Since tr is modular, it must hold that tr((D, W1)) = ~ U {a}. Since tr is faithful, the unique stable AE-expansion b. of ~ U {a} is b. = E( {a, b} ). By the definition of stable expansion we thus have

Since b E b., it follows that

By applying the deduction theorem, we get

In other words,

It thus holds that

Now, since tr is modular, it must hold that tr((D, W2)) = ~ U {a -+ b} . Furthermore, since (D, W1) and (D, W2) both have the same unique de­ fault extension cons( {a, b }), their respective translations tr((D, W1)) and tr((D, W2)) both have the same unique stable expansion b. . In particular, since b. is a stable expansion of tr( (D, W2)) = ~ U {a -+ b}, it holds that

By Equations (5) and (6), it follows that

But this means that b. is a stable AE-expansion of of~­ By the faithfulness of tr, it follows that cons( {a, b}) =

Ll n C is a default extension of (D, W0 ), which is obvi­ ously not true. Contradiction. A modular and faithful translation from default logic to standard AEL is thus impossible. 0

Note that the above negative result also holds for the class of justification-free defaults, i.e., defaults with em­ pty justifications. To see this, just replace a-+ba: M a by a:b : and a : Mb by ab: in the above proof. Note that justification-free defaults are ordinary inference rules. Hence, even ordinary rule systems cannot be faithfully translated into autoepistemic logic. This shows where the real problem lies and hints at how we may restrict default theories in order to obtain modular translatabi­ lity: to prerequisite-free defaults .

For prerequisite-free defaults, we may consider Kono­ lige's most intuitive translation-scheme r:

Theorem 2.2 T is a faithful, modular, and polyno­ mial translation from the class of prerequisite-free default theories to standard AEL.

PROOF. (Sketch) The proof follows directly from pre­ vious results (Theorems 4.1.2 and 4.1.4) by Marek and Truszczirisky [11]; the result is also implicitly present in the work of Lin and Shoham [9]. 0

Some authors argue that prerequisite-free defaults are the only natural defaults. Delgrande and Jackson [1], for instance, define P-Default Logic based in prerequisite­ free defaults. By the above result, P-Default Logic is modularly translatable into standard-AEL.

Note that in Definition 2.2 we defined a rather weak concept of modularity. Stronger types of modularity would require that each single default be separately translatable. Since we proved that even weakly modular translations in the sense of Definition 2.2 are impossi­ ble, the impossibility of any stronger type of modular translation follows .

3 The Non modular Translation

In this Section, we present a faithful polynomial-time translation from default logic to standard AEL. By the results of the last section, such a translation must be nonmodular. In fact, our translation is rather involved and is based on sophisticated propositional coding tech­ niques. It heavily exploits the self referential introspec­ tive capabilities of AEL. For space limitations, we must omit most of the formal details and proofs and can only present the main ideas. The full development can be found in the extended report [4] which is already availa­ ble from the author.

We start by giving an informal rationale of the trans­ lation.

3.1 Rationale of the Translation

Marek, Schwarz and Truszczyriski [12; 20; 19] have exhi­ bited different faithful polynomial translations from de­ fault logic to nonmonotonic N, a variant of AEL which we will define below. We will use a translation t from default logic to nonmonotonic N as an intermediate step in our development. The translation t we use is just a slightly modified version of the translation intro­ duced by Truszczyriski in [20]. Our modification just makes sure that the translation also works for the in­ consistent expansion, which is disregarded in [12; 20; 19] .

Since default logic is translatable via t to nonmono­ tonic N, it suffices to establish a faithful translation h from nonmonotonic logic N to standard AEL. Then, our desired translation e from default logic to standard AEL is obtained by composing t and h, i.e., e = hot . This is illustrated in Fig. 1.

e=. hot

Figure 1: Schema of transformation composition

Nonmonotonic N is stronger than standard AEL in the following sense. Each N-expansion of a set of premi­ ses E is also a standard-AEL-expansion. On the other hand, E may have several additional standard-AEL ex­ pansions which are not N-expansions . These additional expansions are in a certain sense weakly grounded and should be eliminated. In order to get rid of these unde­ sired expansions, we define, for each theory E a formula G(E), the so called grounding formula. In the context of a particular standard-AEL expansion, G(E) has the following intuitive meaning:

In other terms, in the context of each AEL-expansion E of E, the formula G(E) is true if Eisa N-expansion, and false if E is not an N-expansion, i.e., if E is a weakly grounded expansion.

It is now easy to cut off the undesired weakly groun­ ded expansions. The trick is to add the formula LG(E) to E. LG(E) will be a tautology in the context of an N­ expansion of E and therefore harmless. In the context of a consistent weakly grounded expansion of E, howe­ ver, LG(E) evaluates to L false, which is inconsistent and forces the expansion to vanish. It therefore holds that the N-expansions of E exactly correspond to the standard-AEL-expansions of E U {LG(E)}. Our trans­ formation his thus simply obtained by adding LG(E) to E.

We are thus able to enforce groundedness by just ad­ ding a single belief LG(E) to a theory, where LG(E) informally states "I believe that I am a grounded (i.e., N-) expansion of E" . This strong power of beliefs has interesting philosophical interpretations that we will dis­ cuss in Section 4. In the rest of Section 3, we will outline the formal development of the translation.

3.2 Formal Preliminaries

Let C be an ordinary propositional language over a coun­ tably infinite alphabet of propositional variables, the syntactic operators ...,, /1., V, -, +-+, T, and .l (where T is a constant for truth and .l is a constant for fal­ sity). The classical propositional logic over C is denoted by PL(C). The language CL of autoepistemic logic ex­ tends C by a unary modal operator L. The classical propositional logic over the language CL is denoted by PL(CL). For S CCL, SL denotes the set of all subfor­ mulas of the form Lf/J of each formula of S. If ifJ E C L then f/JL =def {ifJJL.

The (monotonic) modal logic N is defined over the samee language C L as standard AEL. N is defined by the axioms of propositional calculus, modus ponens and the necessitation rule ifJ/ Lf/J. N can be considered as the simplest modal logic. A detailed study of N is carried­ out in [3], where also an appropriate Kripke semantics for this logic is defined. The consequence relation according to N is denoted by N. The consequence set operator consN of N is defined in the usual way : if S ~ CL, then consN(S) = { ifJ IS IN ifJ }. Clearly, consN is a monotonic operator .

The nonmonotonic version of N (also called iterative AEL) is defined from monotonic N according to Mc­ Dermott's general definition scheme for nonmonotonic modal logics [13]. The basic concept is the one of an N-expansion. a ~ CL is an N-expansion (also called iterative expansion) of E iff a satisfies the fixed point equation a = consN(E U ...,£a) . It was shown in [12] that each N-expansion of a set E ~ CL is also a stable AEL-expansion of E. The converse does not hold.

The kernel A of a stable expansion a of E is defined by

The following proposition shows that N-expansions can be characterized by special properties of their kernels:

Proposition 3.1 ([5; 10]) Let a be a stable expansion of E and let A be the kernel of a. a is an N -expansion ofE iffEuA- IN A+, where A-= {...,Ll/JI...,Ll/J E A} and A+ = { Lf/J I Lf/J E A} .

For the sake of a simpler notation, we will sometimes implicitly identify finite sets and conjunctions of propo­ sitional formulas.

3.3 Expressing N-inference in PL(C)

In this subsection we outline how inference problems in modal logic N can be polynomially transformed into the problem of tautology-checking in ordinary propositional logic.

Definition 3.1 LetS CCL be a finite set formulas and let ifJ E CL be a formula. A set K ~ SL U ¢JL is called S­ f/J-closed if S UK V= ifJ and for each L'l/; E ( SL U l/JL)- K, su /{ V= 1/J.

Lemma 3.1 S IN ifJ iff there is no S-¢J-closed set.

In order to translate N into classical propositional lo­ gic, we proceed in two steps. In the first step we con­ struct a formula F+ ( S, ifJ) over the language C L such that S IN ifJ iff F+ (S, ifJ) is a propositional tautology in

PL(C£). In the second step, we transform F+(S,¢J) by a simple renaming of variables into an ordinary propositio­ nal formula F(S, ifJ) (over language C) such that F(S, ifJ) is a tautology in PL(.C) iff F+(S,ifJ) is a tautology in PL(CL)

Since we will need a number of additional propositio­ nal variables for constructing F+ ( S , ifJ), let us adopt the following convention . If p E C is an ordinary proposi­ tional variable, then for each formula r E CL, p"' deno­ tes a new distinct propositional variable from C. For l/J, r E CL' ifJ"' denotes the formula obtained from ifJ by uniformly replacing each occurrence (at all levels of L­ nesting) of any ordinary propositional variable p in ifJ by p"~ . If S C CL is a finite set of formulas and r E CL, then s-r = /\.pes ..p-r.

Definition 3.2 Let S C CL be finite and ifJ E CL. For each L'I/J E sL u l/JL' let U.p denote a new distinct pro­ positional variable. Let z be a propositional variable not occurring inS or f/J. Then F+(S, ifJ) is defined to be the formula

Intuitively, this formula states that for each truth va­ lue assignment to the u.p, i.e., for each subset K of sL u l/JL' at least one disjunct must be true , hence K is not S-f/J-closed.

Theorem 3.2 S N ifJ iff F+ ( S, ifJ) is a tautology in PL(CL)

Finally, we transform F+ ( S, ifJ) into a formula F( S, ifJ) which does not contain any modal atoms. If L'l/; is a mo­ dal atom, then [L'I/;] denotes a new distinct propositional variable from C. If U is a formula of PL(CL) , then [U] is the formula obtained from U by uniformly replacing each occurrence of any subformula of the form L'l/; of U not appearing in the scope of some £-operator by [L'I/;] .

Definition 3.3 F(S, ifJ) is defined to be the formula (F+(s, ifJ)J.

Note that F(S, ifJ) E C, since this formula is obtained from F+ ( S, ifJ) by uniformly replacing all atoms L'l/; by ordinary propositional atoms [L'I/;].

Theorem 3.3 S N ifJ iff F(S, ifJ) is a tautology in PL(C).

Remark: The size of F(S,f/J) is at most quadratic in the size of S plus the size of f/J . Thus, deciding S N ifJ is coNP-complete.

3.4 Translating Nonmonotonic N into standard AEL

Our aim is, given a set of premises E, to find a formula G(E) such that the consistent stable AE-expansions of E U LG(E) exactly coincide with the consistent N­ expansions of E. The formula G(E) will enforce any stable AE-expansion to be grounded. More specifically, G(E) will make sure that for each stable expansion Ll of E U G(E) with kernel A it holds that E U A- N A+ , hence, by Proposition 3.1, Ll is an N-expansion.

For any premise set E <; CL we denote by CEXP(E) the set of all consistent standard-AE-expansions of E. The following theorem - fundamental to our transfor­ mation - elucidates the relationship between CEXP(E) and CEXP(E U {La:}) for autoepistemic formulas o: of a certain type. In particular, the theorem shows, how by adding La: to E certain expansions of E can be sup­ pressed.

Theorem 3.4 (Expansion Cutting Theorem)

Given a set E <; CL and a formula o: E CL such that La: f/. EL and any atom of o: is either a propositional va­ riable not occurring in E or an atom L'I/J E EL, it holds that

a.) CEXP(E U {La:}) <; CEXP(E)

• b.) Let Ll E CEXP(E) be a stable AE-expansion of E with kernel A. Let O:A be the propositional formula obtained from o: by replacing each atom L'I/J of o: by T if L'I/J E A and by l. if ·L'I/J E A. Th en Ll E CEXP(E U {La:}) iff O:A is a propositional tautology.

We are now ready for defining the grounding formula G(E) .

Definition 3.4 (Grounding Formula) Let E C CL be a finite set of premises. Assume that z is a propo­ sitional variable not occurring in E . Then G(E) is the formula displayed in Figure 2.

In the proof (given in [4]) of the next theorem, the fol­ lowing is shown. In the context of each part icular AEL­ expansion of E with kernel A, the grounding formula G(E) becomes equivalent to the formula F(E U A- , A+) . Thus , by Theorem 3.3, G(E) is valid iff E U A- N A+ , i.e., iff the expansion corresponding to A is an N­ expansion. The Expansion Cutting Theorem (Thm. 3.4) then guarantees that the theory E U LG(E) has as standard AEL-expansions exactly the N-expansions of E.

Theorem 3.5 Let E C CL be a finit e set of premises. Then Ll is a consistent N -expansion of E iff Ll is a con­ sistent stable AE-expansion of E U { LG(E)}.

We have thus established a polynomial-time transla­ t ion from Nonmonotonic N to Standard AEL.

3.5 Translating Default Logic to standard AEL

Our transformation t from default logic to nonmonotonic N is as follows.

Definition 3.5 Let (D, W) be a default theory. Let v be a propositional variable from C which does not oc­ cur in (D, W) . For each default in d E D of the form o:: M/31, Mf32, .. . ,Mf3n/w, let t(d) denote the autoepistemic formula ( ·Lv 1\ La: 1\ L-,L·/31 1\ ... 1\ L·L'f3n) -+ w. Define the translation t((D, W)) by t((D,W))=WU{t(d) : dED}.

This translation is a slightly modified version of Truszczynski's translation [20]. It handles properly the inconsistent expansion which is disregarded in [20] . By results in [20], it is easy to see that this translation is indeed a faithful embedding of default logic into non­ monotonic N . We now present the definitive translation function e between default logic and standard AEL.

Definition 3.6 If (D, W) is a default theory then e((D, W)) = t((D, W)) U {LG(t((D, W)))}.

Theorem 3.6 (Faithful Translation) The extensions of a default theory (D, W) are given by the sets Ll n C, i.e., the objective parts of Ll, where Ll is a stable AE-expansion of e((D, W)) .

Theorem 3.6 establishes a faithful polynomial trans­ lation from default logic into standard AEL. It is easy to see that a faithful translation in the opposite direc­ tion is not possible. Just consider the autoepistemic theory E = {Lp-+ p} . E has two stable AE-expansions whose objective parts are respectively 0 1 = cons(0) and 02 = cons( {p }). Obviously, 01 C 02. However , it is well known (and follows easily from the definition of default-extension [16]) that no extension of a default theory (D, W) can be a subset of any other extension of (D, W) . Thus, the stable AE-expansions of E do not correspond to the extensions of any default theory. If the expressive power of a nonmonotonic logic stands for its capacity of expressing sets of propositional theories (i .e., sets of alternative epistemic states) through sets of premises, then the expressive power of standard AEL is strictly higher than that of default logic .

4 Philosophical Remarks and Conclusion

Our translatability result admit a somewhat speculative, but nevertheless very appealing and intriguing philoso­ phical interpretation .

Recall that standard AEL is a logic for expressing be­ liefs , and that a set of premises E is conceived as the set of initial beliefs of an ideally rational agent . Hence , the addition of the formula LG(E) to a theory E can be interpreted as the belief of the agent that its own beliefs (w.r.t . E) must be sufficiently grounded in E. We have shown in this paper that the addition of this formula effectively enforces all beliefs based on E to be sufficiently grounded in E . Hence, we delivered a ma­ thematical proof for the fact that (polynomially many) beliefs in groundedness-principles about a theory may control the way of reasoning on the basis of that theory. In particular, if we agree that more strongly grounded expansions are "better" (i .e. , more rational or more sci­ entific) than weakly grounded expansions, then our re­ sult may be paraphrased as follows : an autoepistemic agent can improve its way of reasoning by believing in better principles of reasoning.

Figure 2: The Grounding Formula G(E)

A yet different interpretation or use of our results con­ cerns the problem of communicating knowledge to an au­ toepistemic agent. If we tell a story E to such an agent, we must be prepared to the possibility that the agent bases weakly grounded beliefs on E and acts according to such beliefs. In order to restrict the agent's phantasy and put its feet back on the ground, it is sufficient to add the formula LG(E) to the intended information E.

When we spoke about groundedness in this section, we referred to the type of groundedness inherent in default logic and in the McDermott-style nonmonotonic logics . This kind of groundedness basically limits the "jump" to new nonmonotonic conclusions to such sentences which are obtained by negative introspection. In our opinion, this is a very natural type of groundedness . A more complex (and in our opinion slightly less natural) con­ cept of groundedness underlies the definition of modera­ tely grounded autoepistemic expansion introduced in [8] . A moderately grounded expansion E of ~ is an AE­ expansion of E whose objective part obj(E) is mini­ mal in the following sense: there does not exist any stable set containing E whose objective part is strictly included in obj(E) . Reasoning with moderately groun­ ded expansions is extensively studied in [2] where it is shown that the main reasoning tasks in this formalism are one degree harder in the Polynomial-time Hierarchy than the analogous reasoning tasks in AEL or default logic. For example, checking whether a set of premises has a moderately grounded expansion is Ef -complete [2] , while the analogous reasoning tasks in standard AEL and in default logic are ~f -complete [5] . Thus, unless the Polynomial-time Hierarchy collapses, there cannot exist any polynomial-time embedding (modular or not) of moderately-grounded AEL into standard AEL.