A Tableau Algorithm for Paraconsistent and Nonmonotonic Reasoning in Description Logic-Based System

Abstract. This paper proposes a paraconsistent and nonmonotonic extension of description logic by planting a nonmonotonic mechanism called minimal in-consistency in paradoxical description logics, which is a paraconsistent version of description logics. A precedence relation between two paradoxical models of knowledge bases is firstly introduced to obtain minimally paradoxical mod-els by filtering those models which contain more inconsistencies than others. A new entailment relationship between a KB and an axiom characterized by minimal paradoxical models is applied to characterize the semantics of a para-consistent and nonmonotonic description logic. An important advantage of our adaptation is simultaneously overtaking proverbial shortcomings of existing two kinds extensions of description logics: the weak inference power of paraconsis-tent description logics and the incapacity of nonmonotonic description logics in handling inconsistencies. Moreover, our paraconsistent and nonmonotonic exten-sion not only preserves the syntax of description logic but also maintains the de-cidability of basic reasoning problems in description logics. Finally, we develop a sound and complete tableau algorithm for instance checking with the minimally paradoxical semantics.