A proof-theoretic account of model-preference default reasoning

The "model-preference" account of default reasoning recently proposed by Selman and Kautz overcomes many limitations of previous default formalisms, as it has a strong model-theoretic flavour and provides a formal justification for the limited cognitive load that default reasoning seems to require of human beings. In this paper we describe L(D?+), a non-standard proof system for model-preference default reasoning; L(D?+) is non-standard in the sense that rules have a global (instead of the usual local) character, and that it deals with proofs of the minimality of object level theories rather than with proofs of the theoremhood of formulae. Nonetheless, L(D?+) retains the essential character of a proof system; namely, the independence of provability from the order of application of the rules, and may thus prove a useful tool for the integration of this model-preference default reasoning with other forms of reasoning that are typically dealt with proof-theoretically.