The completeness of reasoning algorithms for clause sets in description logic ALC

• Published in: Knowledge-based systems 2024-02, Vol.286, p.111405, Article 111405
• Main Authors: Kaneiwa, Ken, Takahashi, Daiki
• Format: Article
• Language: English
• Subjects: Automated reasoning; Clausal reasoning; Conjunctive normal form; Description logic ALC; Web ontology language
• ISSN: 0950-7051; 1872-7409
• DOI: 10.1016/j.knosys.2024.111405

Metadata and ontologies are used to enable computers to read data on the Semantic Web. Description logics provide formal languages and reasoning algorithms for such metadata and ontologies. Tableau-based algorithms have been developed for deciding concept satisfiability in description logics but they lead to inefficient reasoning for complex logical expressions. The resolution principle and the Davis–Putnam–Logemann–Loveland (DPLL) solve the weakness by treating simplified clausal forms in description logics. However, resolution-based reasoning for description logics causes to compute various combinations of clause pairs to branch on. On the other hand, DPLL-based approaches have not presented a complete and decidable reasoning algorithm for directly deciding the satisfiability of clauses in description logics. In this paper, we propose a decidable and complete reasoning algorithm for clauses in description logic ALC. Using DPLL techniques, this algorithm can reduce reasoning steps for conjunctive normal form (CNF) concepts in ALC. We prove the termination, soundness, and completeness of the reasoning algorithm for the satisfiability of CNF concepts by introducing a restricted tableau for CNF concepts. We show some examples of reasoning steps for applying clauses in ALC to the algorithm.