1. T = Cn(T);

$$2.\ \ f o r\ \ e w\,e r y\ \varphi$$

B, if v

$$t h e n\ .$$

T then B φ

$$B\,\varphi\quad T\,;$$
$$g.\ \ f o r\ \ e v\,e r y\ \varphi$$

B, if v T then  B φ

$$B\,\varphi\quad T\,.$$

We recall that a stable set T corresponds to a maximal universal Kripke structure MT
such that T is the set of formulas satisfied by MT (Marek & Truszczynski, 1993). With the term AEL model for Σ we will thus refer to a set of interpretations M whose set of theorems Th(M) corresponds to a stable expansion for E in AEL.

Finally, notice that we have adopted the notion of consistent autoepistemic logic (Marek
& Truszczyński, 1993), i.e. in (1) we do not allow the inconsistent theory T =
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 MBNF, allowing in Definition 2.1 the empty set of interpretations to be a possible component of MBNF structures.

In the following, we use the term embedding (or translation) to indicate a transformation function r( ) for modal theories. We are interested in finding a faithful embedding (Gottlob, 1995; Schwarz, 1996; Janhunen, 1998), in the following sense: r( ) is a faithful embedding of AEL into MBNF if, for each theory Σ
B and for each model M, M is an AEL model for Σ iff M is an MBNF model for τ(Σ).

It is already known that AEL theories can be embedded into MBNF theories. In particular, it has been proven (Lin & Shoham, 1992; Schwarz & Truszczyński, 1994) that AEL theories with no nested occurrences of B (called flat theories) can be embedded into MBNF ; now, since in AEL 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 AEL theory can be embedded into MBNF.

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

We first define the translation r( ) of modal theories from AEL to MBNF theories.

B. Then, r(g) is the MBNF formula obtained from cp by substi¬
Definition 3.3 Let φ tuting each occurrence of B with   not.  Moreover, if Σ
B, then T(Σ) denotes the MBNF
theory  BT(ϕ) ϕ  Σ .

We now show that the translation τ( ) embeds AEL theories into MBNF. To this aim, we exploit the semantic characterization of AEL defined by Schwarz (1992). Roughly speaking, according to such a preference semantics over possible-world structures, an AEL model for Σ is a set of interpretations M satisfying Σ such that, for any interpretation J not contained in M the pair ( J t M ) does not satisfy E. Formally:
Proposition 3.4 (Schwarz, 1992, Proposition 4.1) Let E
B. Then, M is an AEL
model for Σ iff, for each interpretation I   M , (I, M) = Σ and, for each interpretation M, (J, M) = Σ.