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

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

作　　者：蒋运承[1,2] 唐素勤[3] 

机构地区：[1]华南师范大学计算机学院,广州510631 [2]中国科学院计算机科学国家重点实验室,北京100190 [3]广西师范大学计算机科学与信息工程学院,广西桂林541004

出　　处：《计算机学报》2009年第8期1500-1510,共11页Chinese Journal of Computers

基　　金：国家自然科学基金(60663001;60573010);中国科学院计算机科学国家重点实验室开放课题基金(SYSKF0904);广西自然科学基金(桂科青0640030;桂科自0991100;桂科自0832103)资助~~

摘　　要：分析了描述逻辑非标准推理的重要性,特别分析了描述逻辑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）.

关 键 词：描述逻辑 n-元存在量词 描述树 描述图 非标准推理 MSC 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]