On the Satisfiability of Quasi-Classical Description Logics

Year, pages: 2017, 1415 - 1446

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.

Zhang, X., Feng, Z., Wu, W., Hossain, M., Maccaull, W. 2017. On the Satisfiability of Quasi-Classical Description Logics. In Computing and Informatics, vol. 36, no.6, pp. 1415-1446. 1335-9150. DOI: https://doi.org/10.4149/cai_2017_6_1415

Zhang, X., Feng, Z., Wu, W., Hossain, M., Maccaull, W. (2017). On the Satisfiability of Quasi-Classical Description Logics. Computing and Informatics, 36(6), 1415-1446. 1335-9150. DOI: https://doi.org/10.4149/cai_2017_6_1415