基于DL-Lite的动态描述逻辑研究

发布时间：2017-09-02 17:08

  本文关键词：基于DL-Lite的动态描述逻辑研究

  更多相关文章： 描述逻辑 动态描述逻辑 可满足性问题 Tableau算法 事务

【摘要】：随着互联网的快速发展及其在人们生活中的普及,描述逻辑受到了国内外越来越多的关注与研究。描述逻辑是一类基于逻辑的知识表示方法,适合于刻画静态领域的知识,有较强的描述能力和可判定性特征,以及有高效的推理算法与推理工具作为支持。然而,仅仅靠描述逻辑不能刻画具有动作特征的问题。研究者提出了各种描述逻辑的各种动态扩展形式,构造出了各种动态描述逻辑。但是,目前所有动态描述逻辑的判定算法中,都限制其中描述逻辑部分的TBox不再包括一般概念包含公理(GCIs),因为一旦引入GCIs,就会导致算法不可判定。DL-Lite是被裁减用于捕获概念建模构造的一种轻量级的描述逻辑,推理复杂度低,易处理,是近年来被推荐作为Web本体语言的OWL2的一个易处理子部分,这些特征使得DL-Lite尤其适合作为大数据下的数据密集型应用的一种概念层。我们从上述两个动机出发,首先选择在DL-Lite上进行动态扩展构造出判定算法支持一般概念包含公理的动态描述逻辑;其次,需要为其提供有效的推理工具;最后,从应用的角度出发,对该逻辑工具进行扩展,研究其典型的应用实例。本文是基于上述思路进行研究工作的,工作主要如下:(1)针对目前动态描述逻辑的判断算法不支持一般概念包含公理的现状,首先,将描述逻辑DL-Lite、动态逻辑和动作理论结合,并限制涉及到角色的包含断言中不能出现否定,构建出了新的动态描述逻辑R prDDL-Lite;然后,给出了其语法与语义,以及为其设计了Tableau算法并介绍算法的整个过程;最后,对其可终止性、可靠性与完备性进行了分析与证明。(2)为了更好的应用于实际问题当中,需要对R prDDL-Lite公式的可满足性问题进行快速简便的判定。因此,在上述R prDDL-Lite的算法基础上开发出相对应的R prDDL-Lite(Tableau)推理机软件,介绍了软件的功能、设计与工具演示,让使用者更容易理解与使用。(3)语义Web下知识库是不断演化的,类比数据库,基于描述逻辑DL-Lite的知识库也同样面临着事务回滚和事务并发的问题,于是在R prDDL-Lite的基础上引入逆动作和并发动作,构建了支持逆动作和并发动作的动态描述逻辑R prCDDL-Lite,研究其在DL-Lite知识库动态演化中的应用。
【关键词】：描述逻辑 动态描述逻辑 可满足性问题 Tableau算法 事务
【学位授予单位】：桂林电子科技大学
【学位级别】：硕士
【学位授予年份】：2015
【分类号】：TP393.09
【目录】：

• 摘要3-4
• ABSTRACT4-9
• 第一章 绪论9-16
• 1.1 研究背景及意义9-11
• 1.2 国内外研究现状11-14
• 1.2.1 描述逻辑11
• 1.2.2 动作理论11-12
• 1.2.3 描述逻辑的动态扩展12-13
• 1.2.4 语义Web、知识库与数据库13-14
• 1.3 研究内容14
• 1.4 论文结构14-16
• 第二章 相关基础知识介绍16-25
• 2.1 描述逻辑DL-Lite16-18
• 2.1.1 描述逻辑概述16-17
• 2.1.2 描述逻辑DL-Lite的语法17
• 2.1.3 描述逻辑DL-Lite的语义17-18
• 2.2 动态描述逻辑D-ALCO18-20
• 2.2.1 动态描述逻辑概述18
• 2.2.2 动态描述逻辑D-ALCO的语法18-19
• 2.2.3 动态描述逻辑D-ALCO的语义19-20
• 2.3 相关推理问题20-22
• 2.3.1 引言20
• 2.3.2 Tableau概述20-21
• 2.3.3 描述逻辑DL-Lite的Tableau判定算法21
• 2.3.4 动态描述逻辑D-ALCO的Tableau判定算法21-22
• 2.4 语义Web、知识库与数据库相关知识22-24
• 2.4.1 语义Web22-23
• 2.4.2 知识库与数据库的比较23-24
• 2.5 本章小结24-25
• 第三章 动态描述逻辑prRDDL-Lite及其可满足性判定算法25-41
• 3.1 引言25
• 3.2 动态描述逻辑prRDDL - Lite25-28
• 3.2.1 prRDDL - Lite的语法25-26
• 3.2.2 prRDDL - Lite的语义26-28
• 3.3 prRDDL - Lite的Tableau判定算法28-32
• 3.3.1 算法预处理28-29
• 3.3.2 算法详细过程29-32
• 3.4 prRDDL - Lite的Tableau判定算法的性质32-38
• 3.4.1 算法的可终止性32-34
• 3.4.2 算法的可靠性和完备性34-38
• 3.5 prRDDL - Lite公式的判定过程实例38-40
• 3.5.1 判定结果为可满足的实例38-39
• 3.5.2 判定结果为不可满足的实例39-40
• 3.6 本章小结40-41
• 第四章 推理机软件的设计与实现41-51
• 4.1 引言41
• 4.2 系统设计与实现41-45
• 4.2.1 开发环境41
• 4.2.2 系统功能41-43
• 4.2.3 系统框架43-45
• 4.3 工具演示45-50
• 4.3.1 工具操作说明45-47
• 4.3.2 概念输入面板47-48
• 4.3.3 动作输入面板48
• 4.3.4 公式输入面板48-49
• 4.3.5 结果显示面板49-50
• 4.4 本章小结50-51
• 第五章 动态描述逻辑prRCDDL-Lite及其可满足性判定算法51-62
• 5.1 引言51
• 5.2 动态描述逻辑prRCDDL - Lite51-54
• 5.2.1 prRCDDL - Lite的语法51-52
• 5.2.2 prRCDDL - Lite的语义52-54
• 5.3 prRCDDL - Lite的可满足性判定算法54-55
• 5.3.1 算法预处理54
• 5.3.2 算法详细过程54-55
• 5.4 prRCDDL - Lite公式的判定过程实例55-58
• 5.4.1 判定结果为可满足的实例55-57
• 5.4.2 判定结果为不可满足的实例57-58
• 5.5 prRCDDL - Lite的Tableau判定算法的性质58-59
• 5.6 prRCDDL - Lite在DL-Lite知识库动态演化中的应用研究59-61
• 5.6.1 事务的概念59
• 5.6.2 事务的prRCDDL - Lite表示59-61
• 5.7 本章小结61-62
• 第六章 结束语62-64
• 6.1 主要研究工作总结62
• 6.2 研究展望62-64
• 参考文献64-68
• 致谢68-69
• 攻读硕士学位期间发表或录用的论文69

【参考文献】

中国期刊全文数据库 前2条

1 梅婧;林作铨;;从ALC到SHOQ(D):描述逻辑及其Tableau算法[J];计算机科学;2005年03期

2 孟小峰,周龙骧,王珊;数据库技术发展趋势[J];软件学报;2004年12期

，

本文编号：779790