Constructive Tightly Grounded Autoepistemic Reasoning

1 Introduction

Nonmonotonic reasoning is one of the most important and active areas of research in knowledge representa­ tion and reasoning. Autoepistemic logic introduced by Moore [1985] appears to be one of the best avail­ able tools for studying nonmonotonic reasoning as re­ cent results [Elkan, 1990; Konolige, 1989; Marek and Truszczynski, 1989] on the relationship betwee~ au­ toepistemic logic and other forms of nonmonotomc rea­ soning suggest that it offers a unifying approach to a large part of nonmonotonic reasoning.

Autoepistemic logic is a modal logic with an operator L which is read 'is believed'. It was originally introduced as a reconstruction of McDermott and Doyle's [1980] nonmonotonic logic to avoid some peculiarities of this logic. Autoepistemic logic models the beliefs of an ide­ ally rational agent who is capable of perfect introspection. The interesting question is to determine the set of beliefs of the agent given a set of formulae as the initial assumptions of the agent. The agent's rationality is in­ terpreted as requiring that the beliefs of the agent have to be logical consequences of the initial assumptions and the beliefs of the agent. The agent is capable of using both positive introspection {if xis a belief, so is Lx) and negative introspection {if xis not a belief, then ...,Lx is). The agent is also ideal: if a formula is a logical conse-. quence of the beliefs of the agent, then it belongs to the set of beliefs of the agent.

*The research has been supported in part by the Jenny and Antti Wihuri Foundation and the Foundation of Technology.

The informal description of the set of beliefs of the agent given above is circular: the set of beliefs is defined using the set of beliefs. Moore [1985] offers a formal def­ inition where the sets of beliefs, the &table expansions of the initial assumptions, are defined as the fixed points of an operator given with the aid of the logical consequence relation used by the agent. Moore's formalization is ele­ gant but in connection with some sets of premises it pr?"" duces sets of beliefs which are quite weakly grounded m the premises. Another problem is that Moore's formal­ ization is non-constructive. It yields no direct method of enumerating or constructing a set of beliefs of the agent given a set of premises. It merely states a condition to be satisfied by any proper set of beliefs based ·on the premises.

We propose a new more constructive definition of the set of beliefs of the agent. It is based on classical logic and enumerations of formulae. It produces sets of beliefs which are a proper subclass of the stable expansions de­ fined by Moore. In fact, the class coincides with iterative expansions defined by Marek and Truszczynski [1989]. Iterative expansions have many desirable properties. In particular, autoepistemic logic based on iterative expan­ sions can be regarded as a generalization of the other leading nonmonotonic logic, default logic [Reiter, 1980]. The basic problem of iterative expansions is that they are not necessarily stable set minimal which suggests that autoepistemic logic based on iterative expansions is not a proper generalization of default logic. This p~o.blem is analysed and shown be the result of the poss1bility of introspecting a formula before introspecting its subfor­ mulae when constructing an iterative expansion. When using the new definition where the enumeration specifies the order of introspection tighter groundedness can be ensured by restricting the order of the formulae in the enumeration, i.e., the order of introspection.

In this paper we propose a new class of expan­ sions based on a special subclass of enumerations, £­ hierarchic enumerations, as the sets of beliefs adopted by an ideal agent with perfect introspection capabili­ ties. L-hierarchic expansions turn out to be more tightly grounded than iterative expansions because they are al­ ways stable set minimal. However, autoepistemic logic based on L-hierarchic expansions still remains a gener­ alization of default logic.

The outline of the paper is as follows. First we in­ troduce autoepistemic logic. Then we present a short survey of the groundedness notions proposed previously. After that we introduce the enumeration based expan­ sions and show that Reiter's default logic is a special case of autoepistemic logic based on L-hierarchic expansions.

2 Autoepistemic logic

We can view autoepistemic logic being induced by some underlying logic CL whose language is .C. In our case CL is the propositional logic. We build an autoepis­ temic logic CL..., on top of CL. We extend .C by adding a monadic operator L and obtain an autoepistemic lan­ guage .Co.e which is the language of CL..., . .Co.e is defined recursively as .C but containing an extra formation rule: if~ E .C...,, then L~ E .Co.e·

Autoepistemic logic models an ideal agent's reasoning about his own beliefs. The agent reasons according to a consequence relation based on the underlying logic and can reflect on his own beliefs. The consequence relation of the underlying logic CL is extended to the richer lan­ guage .Co.e simply by treating L~ formulae as atomic. Thus the consequence relation ~ used by the agent is defined as follows. A formula ~ is a consequence of a set of formulae E (E ~ ~) if ~ is true in every interpretation in which every formula in E is true. The interpretations treat L~ formulae as atomic formulae.

The key objects in autoepistemic logic are the sets of total beliefs of the agent given a set of premises as the agent's initial assumptions. These sets are called &table expansions of the premises and they are the fixed points of an operator defined with the aid of the underlying consequence relation in the following way.

Definition 2.1 [Moore, 1985]!::.. is a stable expansion of E iff!::.. satisfies the following fized point equation.

where L(t::..) = {L~ I~ E !::..}, ...,f:::.. = {...,~I~ E !::..}, and!::..= .C...,-!::... Thus -,£(K} ={-,£~I~ E .C...,-!::..}.

3 Groundedness

It can be argued that stable expansions are too weakly grounded in the premises. We start by an example clar­ ifying the problem.

Example 1 Consider the following premise where p is an atomic formula.

The premise has two stable expansions: one containing p and the other not containing p. The stable expansion containing p can be considered too weakly grounded be­ cause the agent's belief p is based on the fact that the agent believes p, thus obtains Lp by positive introspec­ tion and from this and the premise deduces p. This kind of a belief based on a circular argument is rather weakly grounded in the premises and a stronger form of ground­ edness is often required. ·

In this chapter we survey the various groundedness notions proposed in the literature and show in what re­ spects they are not satisfactory.

Konolige [1988] presents two stronger notions of groundedness leading to moderately grounded and strongly grounded expansions. His basic motivation is to find a class of stable expansions which would capture extensions in default logic [Reiter, 1980] under a suit­ able translation of default logic to autoepistemic logic. To eliminate circularly based beliefs Konolige introduces the concept of a moderately grounded expansion. He shows that a set of formulae !::.. moderately grounded in E is in fact a stable expansion of E which is minimal in the following sense: there is no stable set 1 S which contains E such that S n .C c !::.. n .C, i.e. formulae of S without the L operator are a proper subset of formulae of!::.. without the L operator. Such expansions are said to be stable set minimal for E.

Moderately grounded expansions (or stable set min­ imal expansions) do not quite capture extensions in default logic and, moreover, are still rather weakly grounded as can be seen from the following example also discussed by Konolige [1988].

Example 2 Consider the following set of premises E where p, q are atomic.

E has two stable expansions: one containing p but not q and one containing q but not p. Both are stable set minimal but the first one contains the belief p which is based on the belief p, i.e., the same circular argument as in the previous example. ·

To capture extensions in default logic Konolige pro­ poses the notion of an expansion strongly grounded in the premises. The notion is defined only for autoepis­ temic formulae in a normal form:

where a, p,, and 1 are all in .C. Strongly grounded ex­ pansions are also moderately grounded. However, Marek and Truszcsynski [1989] have discovered that strongly grounded expansions do not capture extensions in de­ fault logic. Marek and Truszcsynski [1989] report that Konolige has introduced a corrected version of the defi­ nition of strongly grounded expansions. Neither defini­ tion of strong groundedness is satisfactory because dif­ ferent expansions could be grounded in different subsets of the premises and strongly grounded expansions de­ pend on the syntactic representation of premises. This means that classically equivalent premises do not have the same strongly grounded expansions. For example, (Lp -+ p) A (-,Lp -+ p) is equivalent top in proposi­ tional logic but the former has none and the latter has one strongly grounded expansion (according to the cor­ rected definition of strong groundedness).

1 A set S is stable if it is closed under propositional conse­ quence and satisfies the conditions (1) if; E S then Lfl E S and (2) if; E S then -,£; E S.

Marek and Truszczynski [1989] present an interesting notion of groundedness in their study of the relationship of default logic and autoepistemic logic. It is based on a monotone operator A defined as follows.

where Cn(E) = {4> I E f= </>}. The operator A is equipped with a context parameter 1:1 ~ lae and given a set of premise E ~ lae the operator A .o. is iterated in the following way.

Marek and Truszczynski [1989] note that A.o.(E) is the set of formulae provable from E U -,£(K) using propo­ sitional logic and the neceBSitation rule. They define a new daBS of expansions based on the operator A.

Definition 3.1 {Marek and Truszczynski [1989]) 1:1 is an iterative expansion of E iff 1:1 = A.o. (E).

They prove that iterative expansions are in fact stable expansions. The daBS of iterative expansions is an at­ tractive candidate for the sets of beliefs adopted by a fully introspective agent. In particular, because in a later paper Marek and Truszczynski [1990]show that iterative expansions generalize nicely reasoning in Reiter's default logic. They show that under the translation trT of the defaults Din a default theory (D, W)

default logic can be seen as a fragment of autoepistemic logic based on iterative expansions, i.e., E is an extension of a default theory (D, W) iff E = 1:1 n l for an iterative expansion 1:1 of trT(D, W).

Marek and Truszczynski [1990] already observed a ba­ sic groundedness problem of iterative expansions and gave the. following example which shows that itera­ tive expansions are not neceBBarily stable set minimal. Thus iterative expansions may be regarded too weakly grounded.

Example 3 Consider a set

where pis atomic. The set E has two stable expansions: one containing p and the other not. Both are iterative but only the second one is minimal. Technically the problem seems to be that the definition of A.o.(E) allows the adoption of a belief (in the context 1:1) which is jus­ tified (indirectly) on the basis of the same belief. This is what happens in the first iterative expansion. H p is put to the context 1:1 but -,£p is not, then by negative intro­ spection we have that -,£-,Lp E A8' (E) and p E A~ (E). Thus Lp E Af>(E). Hence p E A.o.(E) and Lp E A (E). It cannot be the case that -,£p E A .o. (E) (unless A .o. (E) is inconsistent, which it is not). Thus the justification of p is indirectly based on the belief p. ·

Marek and Truszczynski [1989] show how to cap­ ture extensions in default logic using two new classes of expansions: strongly iterative expansions (a strength­ ened form of iterative expansions) and robust expansions. These claBSes of expansions are equivalent with Kono­ lige's strongly grounded expansions and are also defined only for premises in the normal form (4). They suffer from the same unnatural properties as discUBSed in con­ nection with Konolige's strongly grounded expansions, especially, the dependence on the syntactic representa­ tion of premises.

Figure 1 displays a summary of the various grounded­ ness conditions discuBSed above and their relationships. The arrow is interpreted as implies. E.g., strong ground­ edneBB implies stable set minimality.

It seems clear that to get tighter grounded expansions the construction of an expansion should start from the formulae without the L operator. Marek and Truszczyn­ ski [1989] present such a construction which builds a sta­ ble set out of its L-free part. This method does not seem to be applicable to building expansions from premises, however, because expansions cannot be constructed us­ ing such a layered method where, roughly speaking, all formulae having the same depth of L operators are de­ cided at the same time. E.g., consider the set of premises { -,£q-+ q, -,£Lp-+ q}.

Another related idea is to restrict the set of formulae subject to direct introspection and accomplish further introspection by apflying some modal logic. Tiomkin and Kaminski [1990 propose nonmonotonic ground log­ ics based on modal logics T, 84, and 85 where only nega­ tive introspection restricted to L-free formulae is applied directly. The set of beliefs is defined using the following fixed point equation

where 1-s is the derivability relation of the underlying modal logic ( T, 84, SS}. It seems, however, that these ground $-expansions are not neceBSarily stable expan­ sions. E.g., the premise -,£p -+ p has no stable ex­ pansions. But all the underlying logics T, 84, and 85 contain the axiom scheme T (L</> -+ 4>) which produces an S-expansion containing p. So to stay within stable expansions the axiom scheme T has to be abandoned. Konolige's [1988] moderately grounded expansions are an example of these kinds of ground S-expansions. They are based on the modal logic K-45. Unfortunately, the expansions are rather weakly grounded as discussed in Example 2. In fact, it seems that even ground expan­ sions based on the modal logic K have similar problems of weak groundedness as discussed in Example 2. Con­ sider the set of premises {-,Lp-+ q, -,£-,Lp -+ p}. It seems that it has two ground K-expansions: one con­ taining p and the other containing q. However, the first one is quite weakly grounded in the premises.

4 Enumeration Based Expansions

Our aim is to find a proper characterization of the sets of beliefs of an agent with full introspection capabilities. These sets should be stable expansions of the premises but more tightly grounded in the premises. At least they should be stable set minimal and, in addition, mul­ tiple stable set minimal expansions should be excluded in the situations like in Example 2. Iterative exran­ sions suggested by Marek and Truszczynski [1989 are a step in the right direction but are still too weakly grounded as they are not necessarily stable set mini­ mal. Strong iterative expansions (which are the same as strongly grounded and robust expansions) are stable set minimal but are not satisfactory, especially, because of their dependence on the syntactic representation of premises. Another goal is to find a more constructive basis for defining expansions.

We propose a new more constructive definition of the sets of beliefs of an introspective agent which pro­ duces tightly grounded sets of beliefs. The defini­ tion is based on enumerations of the formulae of lae. Davis [1980] used this idea in connection with McDer­ mott and Doyle's [1980] nonmonotonic logic to charac­ terize the intersection of fixed points in McDermott and Doyle's logic. The author [Niemela, 1988] has extended the work of Davis and shown that also individual fixed points in McDermott and Doyle's logic can be charac­ terized using enumerations of the formulae.

The idea is to build a set of beliefs from premises E by applying introspection to formulae in the order given by an enumeration e. A set n·(E) is constructed which contains all the results of introspection in the order e starting from the premises E. The set n·(E) together with E induces the set of beliefs sE· (E) of a fully intro­ spective agent having initial assumptions E after intro­ specting formulae in the order e.

Definition 4.1 Let E ~ lae. Let e = tP1, t/12, ... be an enumeration of all the formulae of lae· Let B~(E) = 0. Define Bt+l (E) for i = 0, 1, ... a& follow&:

B:+ 1 (E) = {BHE) u { Lt/Jt+d if E u Bi{E) F tPHl · Bt{E) U { -,£tPHl} otherwi&e Finally let We would like sE· (E) to be a stable expansion of E induced by the enumeration e. Unfortunately, this not the case for all enumerations.

Example 4 Consider a set of premises

and take an enumeration e = q, p, ... Then B1 (E) = {-,Lq} as E ~ q and n;(E) = {-,Lq,...,Lp} as E u B1 (E) ~ p. But now q E SE· (E) and -,£q E SE· (E) but Lq ¢ SE.(E). Thus SE·(E) does not satisfy the fixed point equation (1) of a stable expansion. ·

To stay within stable expansions we must require enu­ merations to be acceptable in the following sense.

Definition 4.2 An enumeration e i& E-acceptable if there i6 no i and no formula ¢ &uch that -,£¢ E Bt (E) but E U Bi{E) F ¢.

Theorem 4.3 For all E-acceptable enumeration& e, SE.(E) i& a &table u;pan&ion of E.

Proof. We prove that sE· (E) = { ¢ I E u B. (E) F ¢} is a stable expansion of E _by showing that B·(E) = L(SE.(E)) u -,£(SE.(E)).

H Lt/Ji E B.(E), then E u Bt-l(E) F tPi and as Bt-dE) ~ B·(E), tPi E SE.(E) and thus Lt/Ji E L(SE.(E)). H -,£t/Ji E n·(E), then E U Bt_1 (E) ~ tPi· Assume that E u B·(E) F tPi· Then there exists a k ~ i such that E u n:(E) F tPi but -,£.pi E B:(E), which is a contradiction as e is E-acceptable. Thus tPi ¢ SE.(E) and -,£t/Ji E -,£(SE.(E)). This shows that B·(E) ~ L(SE·(E)) u -,£(SE.(E)).

H -,£t/Ji E -,£(SE.(E)), then E u n·(E) ~ tPi· This implies that E uBi-dE) ~ tPi as Bt_1(E) ~ B·(E). Thus -,£.pi E n·(E). H Lt/Ji E L(SE.(E)), then E u B·(E) F tPi· Assume that E u Bt-l(E) ~ tPi· Then there exists a k ~ i such that E u B: (E) F tPi but -,£t/Ji E B:{E), which is a contradiction as e is E­ acceptable. Thus E u Bt-l(E) F tPi and Lt/Ji E B.(E). Hence B·(E) = L(SE.(E)) u -,£(SE.(E)). o

E-acceptable enumerations offer a constructive way to define stable expansions. The expansion is directly built from the premises and the enumeration. It should be noted that even the acceptability condition is in a sense local to each Bi{E) as only those formula t/J; have to be checked for which j :$ i because they are the only formulae for which -,£t/J; E Bt (E) could hold.

However, enumerations are not capable of capturing every stable expansion. Consider the premise Lp --+ p discussed in Example 1. It has two stable expansions: one containing p and the other not containing p. Only the second one is characterizable using enumerations be­ cause in enumeration based expansions Lp cannot be used in deriving p directly. This leads one to assume that enumerations might produce minimal expansions. However, this is not the case as shown by the following example.

Example 5 Consider the set

where pis atomic. I: has two stable expansions which are both characterizable using enumerations. The first one not containing p using an enumeration p, -.Lp, ... and the second containing p using an enumeration -.Lp, p, ... Let us look what happens in the second enumeration ~. B~ (I:) = { -.L-.Lp} as I: ~ -.Lp. But then B; (I:) = { -.L-.Lp, Lp} as I: U BHI:) f= P ·

Thus the enumeration method fails to capture sta­ ble set minimal expansions exactly in the same situa­ tion where iterative method fails. This is no coincidence because enumeration based expansions and iterative ex­ pansions are closely rel<~.ted. Enumerations produce al­ ways iterative expansions and at least for finite sets of premises for every iterative expansion there is a corre­ sponding enumeration producing it.

Theorem 4.4 For all I:-acceptable enumeration.! e, SE~ (I:) i.! an iterative expan.!ion of I:.

Proof. We have to show that for l:l. = SE.(I:), A A (I:) = l:l. holds. First we show that for all i = o, 1, 2, ...

For i = 0 this holds trivially. H Lt/Ji E B:{I:), then I: U B~_di:) f= tPi· By the induction hypothesis I: U L(Af_ 1 (I:)) U -.L(K) f= tPi which implies that t/J· E Af(I:) = Cn(At_ 1 (I:) u L(At_1 (I:))) be­ cause I: U -.L(K) ~ A~ (I:) for all n = 0, 1, ... Thus Lt/J, E L(Af (I:)). H -.L,p, E B:{I:), then tPi ¢ l:l. as ~ is I:-acceptable. Thus -.Lt/J E -.L(I:l.). Hence B: (I:) ~ L( Af (I:)) U -.L(K).

This result implies l:l. ~ A A (I:) in the following way. Let </> E l:l.. Then there exists i such that I: U B~_ 1 (I:) f= <J>. By (14) I: U L(At_ 1 (I:)) U -,£(K) f= </>which implies that</> E Af(I:) ~ AA(I:).

We show that for all i = 0, 1, 2, . . . Af (I:) ~ l:l. which implies AA(I:) ~ l:l. and thus AA(I:) = l:l.. Let </> E A&>{I:). Then I: U -.L(K) f= </>. So </> E l:l. = {</> I I: U L(l:l.) U -.L(K) f= </>}. Let </> E Af(I:). Then At_ 1 (I:)uL(At_ 1 (I:)) f= <J>. By the induction hypothesis At_ 1 (I:) ~ l:l. and thus L(At_ 1 (I:)) ~ L(l:l.) ~ l:l.. Thus </> E l:l.. 0

Theorem 4.5 For each. iterative expan.!ion l:l. of a finite 6et of premi.!u I: there i_, a I:-acceptable enumeration ~ 6Uch. that f:l. = SE· (I:).

Proof . . It can be shown that a I:-acceptable enumer­ ation ~ which induces l:l. can be constructed from l:l. in the following way if I: is finite.

1. Let the first formulae in ~ be the formulae tPi ¢ l:l. for which Lt/Ji E SfL(I:) 2 ·
2. The next formulae in ~ are those tPi E l:l. for which Lt/Ji E SfL(I:) in the order they are produced by the iteration of A A .
3. All the rest of the formulae in .Cae are ordered such that if Lt/Ji E SfL({t/J;}), then i < j.

2 SfL(E) is the set of the Lx aubformulae of the formulae in E.

The set I: has to be finite for the conditions 1 and 2 to be satisfied by an enumeration of formulae. The question whether there exists a I:-acceptable enumeration ~ which induces l:l. for any iterative expansion l:l. of an infinite set of premises I: remains open. 0

Thus enumeration based expansions provide an alter­ native way of defining iterative expansions. Example 5 reveals also why iterative expansions are not necessarily stable set minimal. It is possible to introspect a formula </> without first introspecting the subformulae of </> which can effect the result of the introspection of</>. In the case of Example 5 it is possible to introspect -.Lp and obtain -.L-.Lp without first checking the status of p.

So it seems as a very natural requirement to demand that in order to get tightly grounded beliefs all subformu­ lae of a given formula </> that can effect the result of the introspection of </> must be examined before </>. This new groul).dedness requirement can be incorporated easily to the definition of enumeration based stable expansions. We require the enumerations to be £-hierarchic. This means that a formula </> can appear in the enumeration only after all t/J such that Lt/J is a subformula of </> have appeared in the enumeration. It is unclear how to incor­ porate this kind of a requirement into the definition of iterative expansions.

Definition 4.6 Let ~ be an enumeration t/J1, t/J2, ... of all the formulae in .Cae. e i& L-hierarchic if for all tPi, t/J; hold.! that if Lt/Ji E SfL({t/J;}), then i < j.

Definition 4.1 SE~(I:) i& an L-hierarchic expansion of I: if~ i6 a I:-acceptable £-hierarchic enumeration.

It turns out that the simple requirement on the order of the formulae in the enumerations guarantees that L­ hierarchic expansions are stable set minimal.

Theorem 4.8 Every £-hierarchic expan.!ion SE~ (I:) of I: i.! a &table 6et minimal &table expan&ion of I: {a mod­ erately grounded expan~ion of I:).

Proof. We denote SE.(I:) by l:l.. Assume that there exists a stable set S containing I: such that Sn.C ~ tl.n.C. We prove that l:l. = S by showing that for all i = 1, 2, ... , tPi E fl. iff tPi E S. This proves that fl. is stable set minimal for I:.

H t/J1 E S, then as ~is L-hierarchic t/J1 E .C and t/J1 E fl.. H t/J1 E fl., then I: f= tPl as e is I:-acceptable. Thus t/J1 E S as I: ~ S and S is stable.

H tPi E l:l., then I:UB~_1 (I:) f= tPi as e is I:-acceptable. By the induction hypothesis B~_1 (I:) ~ S. Thus tPi E S as I: ~ S and S is stable. Let tPi ¢ l:l.. The formula tPi can be transformed into a normal form ,p; = d1 1\ · ·· 1\ dn where each~ is of the form

where '1 E .C and a,, p, E .Cae· It holds that tPi E fl. iff ,p; E l:l.. So t/Ji ¢ l:l.. Thus there exists a dis­ junction d; ¢ l:l.. As l:l. is a stable set, d; ¢ fl. iff '1 ¢ l:l., a1 ¢ l:l., ... , am ¢ l:l., /i1 E fl., ... , /i1 E fl.. The normal form transformation does not go into the Lx for­ mulae. Thus SfL({,p,}) = SfL({t/JH) and so each a, and p, is some t/J; such that i < i because the enumer­ ation is L-hierarchic. Thus by the induction hypothesis a1 ¢, 8, ... ,am ¢, 8,{31 E 8, ... ,{3, E 8. As 'Y E f. and 'Y ¢ ~. 'Y ¢ 8. Thus d; ¢ 8 which implies that 1/li ¢ 8. As ,p, is equivalent to 1/li, ,p, ¢ 8. Hence ~ = 8 0

Thus an L-hierarchic expansion of E is a stable set minimal iterative expansion which is not dependent on the syntactic representation of premises. E.g., {Lp -+ p, -.Lp -+ p} and {p} have both the same unique L­ hierarchic expansion. So L-hierarchic expansions are not necessarily strongly grounded (or strongly itera­ tive/robust).

It turns out that in the case ofT-clauses which are of the form

where a,, {3,, 'Y E f. all iterative expansions of every finite set of premises are also L-hierarchic expansions. It can be shown that the conditions in the proof of Theorem 4.5 for an enumeration inducing an iterative expansion are also satisfied by an L-hierarchic enumeration for each it­ erative expansion of every finite set ofT-clauses. So for T-clauses iterative and L-hierarchic expansions coincide. This shows that L-hierarchic expansions are adequate to capture extensions in Reiter's default logic using the translation proposed by Marek and Truszczynski (9) be­ cause this translation produces T-clauses.

Theorem 4.9 E ~ f. u an e:l:ten&ion of a finite de­ fault theory (D, W) 3 iff E = SE·(trT(D, W)) n f. for a trT(D, W)-acceptable L-hierarchic enumeration e.

Thus autoepistemic logic based on L-hierarchic expan­ sions is a generalization of default logic which provides an alternative definition of an extension (Reiter [1980] gave originally a fixed point characterization). On the other hand, default logic is a special case of this kind of autoepistemic logic where only formulae of the form (La A -.LL-.{31 A ··· A -.LL-.f3n) -+ 'Y are allowed.

The question of a general semantics approach to L­ hierarchic expansions remains open. In the case of T­ programs which are T-clauses where a,, p,, 'Y E f. are literals Marek and Truszczynski [1990] have given a se­ mantic characterization of consistent iterative expan­ sions and as in this case iterative and L-hierarchic ex­ pansions coincide this semantics applies also to consis­ tent L-hierarchic expansions ofT-programs.

5 Conclusions

We have introduced a new class of expansions in au­ toepistemic logic called £-hierarchic expan&ion&. L­ hierarchic expansions are very promising candidates for the sets of conclusions derived by an ideally rational agent with full introspection capabilities on the basis of given premises. This new class of expansions has a number of attractive properties. Instead of a fixed point characterization an L-hierarchic expansion is con­ structed directly from the premises and an enumeration of the formulae of the language. The construction is given in terms of classical logic, e.g., no modal logic is needed. L-hierarchic expansions are independent of the syntactic representation of premises. They are very tightly grounded in the premises. They are iterative ex­ pansions [Marek and Truszczynski, 1989] and, in addi­ tion, always stable set minimal. Furthermore, autoepis­ temic logic based on L-hierarchic expansions captures default reasoning: it is shown that Reiter's default logic is a special case of this new logic. One of the most im­ portant open problems is the question of existence of a semantic characterization of L-hierarchic expansions in the general case.

8 For a finite default theory (D, W) D u W is a finite set.