Default reasoning with a constraint resolution principle

Abstract

Common non-monotonic deduction systems such as Reiters default logic or inheritance networks must handle the multiple extension problem, i.e. generally they have distinct consistent sets of conclusions (extensions) which can be drawn from a theory. Most of these systems do not provide any control structure that helps to determine in which of these extensions inferences are made. Default proof theories are in most cases only able to prove if a sentence is in at least one extension. We create a resolution based system for default reasoning where an explicit control set can be built during reasoning and where default assumptions made in a deduction are remembered as constraints.

The resulting system is a cumulative default logic which assures an even stricter cumulativity than Brewka's Cumulative Default Logic and is strong enough to express Poole's Framework for default reasoning. It turns out that the created system ranges from the logic with restricted quantifiers of H.J.Bürckert via Reiter's default logic to the logic of theory change of Gärdenfors.