An Extended Framework for Default Reasoning

In this paper, we investigate the proof theory of default reasoning. We generalize Reiter's framework to a monotonic reasoning system, and in particular allow formulae with nested defaults. We give proof rules for this extended default logic, called default ionic logic, and give deduction theorems. We also give examples of applications of our framework to some well-known problems: weak implication, disjunctive information, default transformation, and normal versus non-normal defaults. 1 Introduction In this paper we investigate the proof theory of default reasoning. We have as a goal a general theory for combining defaults, and a logical tool for choosing among defaults for implementation purposes. The calculus on extensions developed by Reiter [6] has yielded a kind of reasoning that has been called non-monotonic. This non-monotonicity is the source of some major problems for implementers. The applicability of modus tollens, a fundamental tool in resolution, is unclear. For example ..