Nonmonotonic consequence in default model theory
Abstract
Default model theory is a nonmonotonic formalism for representing and
reasoning about commonsense knowledge. Although this theory is motivated by ideas in
Reiter’s work on default logic, it is a very different, in some sense dual framework. We
make Reiter’s default extension operator into a constructive method of building models,
not theories. Domain theory, which is a well established tool for partial information in the
semantics of programming languages, is adopted as the basis for constructing partial models.
One of the direct advantages of default model theory is that nonmonotonic reasoning can be
conducted with monotonic logics, by using the method of model checking, instead of theorem
proving.
This paper reconsiders some of the laws of nonmonotonic consequence, due to Gabbay
and to Kraus, Lehmann, and Magidor, in the light of default model theory. We remark
that in general, Gabbay’s law of cautious monotony is open to question. We consider an
axiomatization of the nonmonotonic consequence relation omitting this law. We prove a representation
theorem showing that such relations are in one to one correspondence with the
consequence relations determined by extensions in Scott domains augmented with default
sets. This means that defaults are very expressive: they can, in a sense, represent any reasonable
nonmonotonic entailment. Results about what kind of defaults determine cautious
monotony are also discussed. In particular, we show that the property of unique extension
guarantees cautious monotony, and we characterize default structures which determine
unique extensions.