带n-元存在量词的描述逻辑MSC推理

Computing Most Specific Concept in Description Logic with n-Ary Existential Quantifier

分析了描述逻辑非标准推理的重要性,特别分析了描述逻辑MSC(Most Specific Concept)推理的研究现状和存在的问题.针对目前描述逻辑MSC推理不能处理n-元存在量词的不足,研究了带n-元存在量词的描述逻辑εL(n)的MSC推理问题.提出了一种新的εL(n)-描述图,利用描述树和描述图给出了描述逻辑εL(n)的MSC近似推理算法,并利用εL(n)-描述树嵌套和εL(n)-描述树描述图同态证明了MSC近似推理算法的正确性.作为一个附带的结果,利用εL(n)-描述树描述图同态给出了εL(n)的实例推理算法,也证明了实例推理算法的正确性.

Description Logics （DLs） are a logical reconstruction of the frame-based knowledge representation languages, with the aim of providing a simple well-established declarative semantics to capture the meaning of structured representation of knowledge. The fundamentality of non-standard inferences in DLs, especially the current research progress and the existing prob- lems of the MSC （Most Specific Concept） inference in DLs, are analyzed in this paper. Aiming at the insufficiency of the MSC inference in DLs which can not deal with n-ary existential quantifier, the MSC inference for the DL with n-ary existential quantifier εL^（n） is studied, where n-ary existential quantifier is a new concept constructor in DLs. A kind of new εL^（n）-description graph is presented. The inference algorithm of approximating MSC in εL^（n） is presented using description tree and description graph, and the correctness of inference algorithm of approximating MSC is proved using εL^（n）description trees embedding and εL^（n）-description tree and description graph homomor-phism. As a by-product, the instance reasoning tree and description graph homomorphism, and algorithm in εL^（n） is presented using εL^（n）-description the correctness of instance reasoning algorithm is also proved. Theoretical foundation for the MSC inference for more expressive DLs with n-ary existential quantifier such as CLU^（n） and ALε^（n） is provided through the MSC inference algorithm of εL^（n）.