Default description logics with reversing inference rules

Default description logics are extensions of description logics by Reiter's default logic in order to represent and reason about non-monotonic knowledge. A default says that if its prerequisite is provable, and the negation of its justification is not provable, then its consequence is provable. As a method of using defaults in a reverse way, reversing inference rules are introduced to default description logics. For a default, its reversing inference rule says if the negation of the consequence of the default is provable, then the negation of the prerequisite or the negation of the justification of the default is provable. Then a default description theory is extended to an extended default description theory with reversing inference rules and the definition of extensions of the extended default description theory is given. A default description theory can infer statements by using its defaults. However, an extended default description theory can infer statements not only by using its defaults, but by using its reversing inference rules. The relations between default description theories and their extended default description theories are discussed. For a default description theory without extensions, its extended default description theory may have extensions.