Complexity of power default reasoning

This paper derives a new and surprisingly low complexity result for inference in a new form of Reiter's propositional default logic (1980). The problem studied here is the default inference problem whose fundamental importance was pointed out by Kraus, Lehmann, and Magidor (1980). We prove that "normal" default inference, in propositional logic, is a problem complete for co-NP(3), the third level of the Boolean hierarchy. Our result (by changing the underlying semantics) contrasts favorably with a similar result of Gottlob (1992), who proves that standard default inference is II/sub 2//sup P/-complete. Our inference relation also obeys all of the laws for preferential consequence relations set forth by Kraus, Lehmann, and Magidor (1990). In particular we get the property of being able to reason by cases and the law of cautious monotony. Both of these laws fail for standard propositional default logic. The key technique for our results is the use of Scott's domain theory to integrate defaults into partial model theory of the logic, instead of keeping defaults as quasiproof rules in the syntax. In particular, reasoning disjunctively entails using the Smyth powerdomain.