Quasi-Classical Description Logics and Paraconsistent Tableau Calculus for Reasoning with Acyclic Tbox

The forthcoming semantic Web evolving from the current World Wide Web is designed to define the semantics of information and services on the web, thereby endowing the web with intelligence to automatically reason about the web contents. Description logics (DLs) play a substantial role in the semantic Web, since they underlie the W3C-recommended Web ontology language (OWL), which is derived from ontology research in artificial intelligence (AI) in order to achieve the goal of the semantic Web. However, the knowledge and data in the Semantic Web are large-scale, dispersive, multi-authored, and therefore usually inconsistent. It is reasonable and imperative to develop practical reasoning techniques for inconsistent ontologies. This paper proposes a new type of paraconsistent description logics based on Hunter's quasi-classical logic (QCL), which are termed as quasi-classical description logics (QCDLs). QCDLs avoid logical explosion. A semantic tableau calculus is constructed in QCDLs for the reasoning on the knowledge bases with acyclic TBox. Furthermore, a sound, complete and decidable consequence relation based on the calculus is defined. These enable a complete framework for paraconsistent reasoning in the Semantic Web. A comparison with other key paraconsistent description logics is also given. It is shown that QCDLs possess more expressive semantics and stronger reasoning capability, and that its connectives behave classically at the object level.