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.

翻译：在语义网页上,使用元数据和文理来使计算机能够读取数据。已经提议将网络本体语言(OWL)作为标准的本体语言,并研究了该语言的各种推论系统。描述逻辑被视为OWL的理论基础;它们为描述本体和知识基础提供了正式语言的语法和语义。此外,描述逻辑的表单算法已经发展成为处理可判问题的标准推理算法。然而,表式算法产生了效率低下的推理步骤,因为其非非决定性的分枝,以及因存在性量化而增加的模型规模。在本研究中,我们提出了对应的正常形式(CNF)概念,这些概念使用统一的概念形式来描述逻辑和知识基础。用一个统一的概念格式来为一系列条款的推理推理法制定算法。我们为各套条款提出了一个有效的推理算法,其中任何LC概念都转换成类似的CNF概念。理论上,我们证明CNF的推理算法概念的正确性、完整性和终结性。