  A fact apparently not observed earlier in the literature of nonmonotonic
reasoning is that Reiter, in his default logic paper, did not directly
formalize informal defaults. Instead, he translated a default into a certain
natural language proposition and provided a formalization of the latter. A few
years later, Moore noted that propositions like the one used by Reiter are
fundamentally different than defaults and exhibit a certain autoepistemic
nature. Thus, Reiter had developed his default logic as a formalization of
autoepistemic propositions rather than of defaults.
  The first goal of this paper is to show that some problems of Reiter's
default logic as a formal way to reason about informal defaults are directly
attributable to the autoepistemic nature of default logic and to the mismatch
between informal defaults and the Reiter's formal defaults, the latter being a
formal expression of the autoepistemic propositions Reiter used as a
representation of informal defaults.
  The second goal of our paper is to compare the work of Reiter and Moore.
While each of them attempted to formalize autoepistemic propositions, the modes
of reasoning in their respective logics were different. We revisit Moore's and
Reiter's intuitions and present them from the perspective of autotheoremhood,
where theories can include propositions referring to the theory's own theorems.
We then discuss the formalization of this perspective in the logics of Moore
and Reiter, respectively, using the unifying semantic framework for default and
autoepistemic logics that we developed earlier. We argue that Reiter's default
logic is a better formalization of Moore's intuitions about autoepistemic
propositions than Moore's own autoepistemic logic.
