Towards an axiom system for default logic

Recently, Lakemeyer and Levesque proposed a logic of only-knowing which precisely captures three forms of nonmonotonic reasoning: Moore's Autoepistemic Logic, Konolige's variant based on moderately grounded expansions, and Reiter's default logic. Defaults have a uniform representation under all three interpretations in the new logic. Moreover, the logic itself is monotonic, that is, nonmonotonic reasoning is cast in terms of validity in the classical sense. While Lakemeyer and Levesque gave a model-theoretic account of their logic, a proof-theoretic characterization remained open. This paper fills that gap for the propositional subset: a sound and complete axiom system in the new logic for all three varieties of default reasoning. We also present formal derivations for some examples of default reasoning. Finally we present evidence that it is unlikely that a complete axiom system exists in the first-order case, even when restricted to the simplest forms of default reasoning.