A proof-theoretic account of model-preference default reasoning

The "modcl-preference" account of default reasoning recently proposed by Selman and Kautz overcomes some limitations of previous default formalisms, as it has a strong model-theoretic flavour and provides a formai justification for the limited cognitive load that default reasoning seems to require of human beings. In this paper we describe L{'])T), a non-standard proof system for model-preference default reasoning; L{'])T) is non-standard in the sense that rules have a global character, and that it deals with proofs of the minimality of knowledge bases rather than with proofs of the theorcmhood of formulae. Nonethelcss, L{'])T) retains the essential character of a proof system, namely, the independence of provability from the order of application of the rules.