Description logic with default reasoning

As a formal tool for knowledge representation and reasoning, description logic provides the decidable reasoning service. This paper proposes a new description logic with default reasoning, which integrates monotonic reasoning and non-monotonic reasoning while avoiding the difficulty of Reiter's default logic. Based on the description logic with default reasoning, we construct a knowledge base system that incorporates Tbox, Abox and default rules. Then we discuss several reasoning problems including concept satisfiability, default satisfiability, concept subsumption, default subsumption, and instance checking. Furthermore, we present a new algorithm called Tableau-D that is used to check the satisfiability and default satisfiability. Finally a transformation theorem of default satisfiability and default subsumption is also attained.