On embedding default logic into Moore''s autoepistemic logic

Recently Gottlob proved [2] that there does not exist a faithful modular translation of default logic into autoepistemic logic, and presented a non-modular translation. Gottlob's translation, however, is indirect (it uses “nonmonotonic logic N” as an intermediate point), quite complex and exploits sophisticated encoding of proof theory in autoepistemic formulas. We provide a simpler and more intuitive (non-modular) direct translation. In addition, our argument is purely model-theoretic.