Alternative foundations for Reiter's default logic (Q1589575)

We introduce an alternative conceptual basis for default reasoning in Reiter's default logic. In fact, most formal or computational treatments of default logic suffer from the necessity of exhaustive consistency checks with respect to the finally resulting set of conclusions; often this so-called extension is just about being constructed. On the theoretical side, this exhaustive approach is reflected by the usual fixed-point characterizations of extensions. Our goal is to reduce such global considerations to local and strictly necessary ones. For this purpose, we develop various techniques and instruments that draw on an analysis of interaction patterns between default rules, embodied by their mutual blocking behavior. These formal tools provide us with alternative means for addressing a variety of questions in default logic. We demonstrate the utility of our approach by applying it to three traditional problems. First, we obtain a range of criteria guaranteeing the existence and non-existence of extensions. Second, we get alternative characterizations of extensions that avoid fixed-point conditions. Finally, we furnish a formal account of default proofs that was up to now neglected in the literature.