We introduce new concepts for default reasoning in the context of query-answering in regular default logic. For this purpose, we develop a proof-orinented approach for deciding whether a default theory has an extension containing a given query. The inherent problem in Reiter's default logic is that it necessitates the inspection of all default rules for answering no matter what query. Also, default theories are known to lack extensions occasionally. We address these two problems by sloting in a compilation phase before the actual query-answering phase. The examination of the entire set of default rules is then done only once in the compilation phase; this allows us to inspect only the utilimately necessary default rules during the actual query answering phase. In fact, the latter inspection must not only account for hte derivability of the query, but moreover it must guarantee the existence of an encompassing extension. We address this traditionally important problem by furnishing novel criteria guaranteeing the existence of extensions that are arguably simpler and go well beyong existing approaches.
展开▼
