On the Satisfiability of Quasi-Classical Description Logics

Authors

  • Xiaowang Zhang School of Computer Science and Technology, Tianjin University, Tianjin & Tianjin Key Laboratory of Cognitive Computing and Application, Tianjin
  • Zhiyong Feng School of Computer Science and Technology, Tianjin University, Tianjin & Tianjin Key Laboratory of Cognitive Computing and Application, Tianjin
  • Wenrui Wu School of Computer Science and Technology, Tianjin University, Tianjin 300072
  • Mokarrom Hossain Department of Mathematics, Statistics and Computer Science, St. Francis Xavier University, PO Box 5000, Antigonish, NS
  • Wendy MacCaull Department of Mathematics, Statistics and Computer Science, St. Francis Xavier University, PO Box 5000, Antigonish, NS

Keywords:

Semantic web, description logics, quasi-classical logic, satisfiability, tableaux

Abstract

Though quasi-classical description logic (QCDL) can tolerate the inconsistency of description logic in reasoning, a knowledge base in QCDL possibly has no model. In this paper, we investigate the satisfiability of QCDL, namely, QC-coherency and QC-consistency and develop a tableau calculus, as a formal proof, to determine whether a knowledge base in QCDL is QC-consistent. To do so, we repair the standard tableau for DL by introducing several new expansion rules and defining a new closeness condition. Finally, we prove that this calculus is sound and complete. Based on this calculus, we implement an OWL paraconsistent reasoner called QC-OWL. Preliminary experiments show that QC-OWL is highly efficient in checking QC-consistency.

Downloads

Download data is not yet available.

Downloads

Published

2018-02-09

How to Cite

Zhang, X., Feng, Z., Wu, W., Hossain, M., & MacCaull, W. (2018). On the Satisfiability of Quasi-Classical Description Logics. COMPUTING AND INFORMATICS, 36(6), 1415–1446. Retrieved from http://www.cai.sk/ojs/index.php/cai/article/view/2017_6_1415