论文标题
描述逻辑alc中的子句集的推理算法的完整性
The Completeness of Reasoning Algorithms for Clause Sets in Description Logic ALC
论文作者
论文摘要
在语义网络上，元数据和本体学用于使计算机读取数据。 Web本体语言（OWL）已被提议作为标准的本体论语言，并研究了该语言的各种推理系统。描述逻辑被视为猫头鹰的理论基础；它们提供了一种形式语言的语法和语义来描述本体和知识基础。此外，用于描述逻辑的Tableau算法已开发为可决定问题的标准推理算法。但是，由于其非确定性分支进行分离以及通过存在量化而导致的模型大小的增加，Tableau算法会产生效率低下的推理步骤。在这项研究中，我们提出了结合性正常形式（CNF）概念，该概念利用平坦的概念形式来描述逻辑ALC，以开发用于推理一组条款的算法。我们为子句集提出了一种有效的推理算法，其中任何ALC概念都转化为同等的CNF概念。从理论上讲，我们证明了推理算法的健全性，完整性和终止，以满足CNF概念。
On the Semantic Web, metadata and ontologies are used to enable computers to read data. The Web Ontology Language (OWL) has been proposed as a standard ontological language, and various inference systems for this language have been studied. Description logics are regarded as the theoretical foundations of OWL; they provide the syntax and semantics of a formal language for describing ontologies and knowledge bases. In addition, tableau algorithms for description logics have been developed as the standard reasoning algorithms for decidable problems. However, tableau algorithms generate inefficient reasoning steps owing to their nondeterministic branching for disjunction as well as the increase in the size of models occasioned by existential quantification. In this study, we propose conjunctive normal form (CNF) concepts, which utilize a flat concept form for description logic ALC in order to develop algorithms for reasoning about sets of clauses. We present an efficient reasoning algorithm for clause sets where any ALC concept is transformed into an equivalent CNF concept. Theoretically, we prove the soundness, completeness, and termination of the reasoning algorithms for the satisfiability of CNF concepts.
