文档介绍：分类号密级 U D C 编号桂林电子科技大学硕士学位论文题目基于OBDD的描述逻辑推理算法研究(英文) Researchon OBDD-based Decision Algorithmsfor DescriptionLogics 研究生学号: 092031119 研究生姓名: 黄聪指导教师姓名、职务: 古天龙(教授) 申请学位门类: 工学硕士学科、专业: 计算机应用技术提交论文日期: 2012 年4月论文答辩日期: 2012年6月年月日独创性(或创新性)声明本人声明所呈交的论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知,除了文中特别加以标注和致谢中所罗列的内容以外,论文中不包含其他人已经发表或撰写过的研究成果;也不包含为获得桂林电子科技大学或其它教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中做了明确的说明并表示了谢意。申请学位论文与资料若有不实之处,本人承担一切相关责任。本人签名: 日期: 关于论文使用授权的说明本人完全了解桂林电子科技大学有关保留和使用学位论文的规定,即:研究生在校攻读学位期间论文工作的知识产权单位属桂林电子科技大学。本人保证毕业离校后,发表论文或使用论文工作成果时署名单位仍然为桂林电子科技大学。学校有权保留送交论文的复印件,允许查阅和借阅论文;学校可以公布论文的全部或部分内容, 可以允许采用影印、缩印或其它复制手段保存论文。(保密的论文在解密后遵守此规定) 本学位论文属于保密在____年解密后适用本授权书。本人签名: 日期: 导师签名: 日期: 摘要 I 摘要描述逻辑是一类刻画领域知识的形式化工具,在信息系统、软件工程、自然语言处理等领域已得到了成功应用。目前描述逻辑已成为语义Web本体语言OWL的逻辑基础,在语义Web中起着更重要的作用。而当前的描述逻辑的推理算法却存在一些缺陷,尤其是在处理大规模问题时表现更为突出。Tableau算法是当前描述逻辑中最主要的推理方法,但其并不是在所有情况下都表现最好。因此,针对不同特征的本体, 寻找合适的推理算法一直备受学者关注。在现有的描述逻辑推理系统中,都要求描述逻辑知识库中的TBox中不包含有循环定义。但是,在很多场合下,不得不用循环定义来对知识进行刻画。如何解决有循环定义的推理问题也是备受关注。有序二叉决策图(OBDD)是一种基于图的数据结构,是布尔函数的一种压缩表示形式,是信息的高效压缩,能高效地处理大规模问题,在模型检测和验证等领域已经得到了广泛应用。基于上述原因,本文做了基于OBDD的描述逻辑推理算法相关研究。其主要内容如下: (1)针对不允许循环定义的描述逻辑ALC,给出基于OBDD的可满足判定算法。首先根据待判定概念的形式,计算出其所有子概念和每个子概念的否定形式的集合; 然后根据该集合里的每个概念的形式构造出其相应的布尔函数;最后将布尔函数转化为OBDD的表示形式来进行概念的可满足性判定;此外,并证明算法的正确性。(2)针对允许循环定义的但不含有否定构造算子的描述逻辑εL循环术语集,给出基于OBDD的不动点语义下的概念包含判定算法。首先根据TBox的描述图和模拟关系,给出最大模拟关系的性质并证明其正确性;然后用OBDD刻画描述图,进而利用OBDD计算最大模拟关系以及循环路径;最后通过OBDD的可满足操作来判定包含关系。(3)针对允许循环定义并且包含否定构造算子的描述逻辑μ ALC,给出基于OBDD 的概念可满足的判定算法。首先构造造出其准模型;然后利用布尔函数表示准模型, 得到准模型的OBDD表示;最后利用基于OBDD的验证算法对准模型进行验证以判定概念可满足性。关键词:描述逻辑;有序二叉决策图;循环术语集;可满足性;不动点语义;包含问题 Abstract II Abstract As a family of knowledge representation formalisms, description logic has been essfully applied in information systems, software engineering, natural language processing and other fields. Description logichas e the logical basis of the Semantic Web Ontology Language (OWL)and playing an important rolein Semantic the rec