本文關(guān)鍵詞：基于DL-Lite的動態(tài)描述邏輯研究

  更多相關(guān)文章： 描述邏輯 動態(tài)描述邏輯 可滿足性問題 Tableau算法 事務(wù)

【摘要】：隨著互聯(lián)網(wǎng)的快速發(fā)展及其在人們生活中的普及,描述邏輯受到了國內(nèi)外越來越多的關(guān)注與研究。描述邏輯是一類基于邏輯的知識表示方法,適合于刻畫靜態(tài)領(lǐng)域的知識,有較強的描述能力和可判定性特征,以及有高效的推理算法與推理工具作為支持。然而,僅僅靠描述邏輯不能刻畫具有動作特征的問題。研究者提出了各種描述邏輯的各種動態(tài)擴展形式,構(gòu)造出了各種動態(tài)描述邏輯。但是,目前所有動態(tài)描述邏輯的判定算法中,都限制其中描述邏輯部分的TBox不再包括一般概念包含公理(GCIs),因為一旦引入GCIs,就會導(dǎo)致算法不可判定。DL-Lite是被裁減用于捕獲概念建模構(gòu)造的一種輕量級的描述邏輯,推理復(fù)雜度低,易處理,是近年來被推薦作為Web本體語言的OWL2的一個易處理子部分,這些特征使得DL-Lite尤其適合作為大數(shù)據(jù)下的數(shù)據(jù)密集型應(yīng)用的一種概念層。我們從上述兩個動機出發(fā),首先選擇在DL-Lite上進行動態(tài)擴展構(gòu)造出判定算法支持一般概念包含公理的動態(tài)描述邏輯;其次,需要為其提供有效的推理工具;最后,從應(yīng)用的角度出發(fā),對該邏輯工具進行擴展,研究其典型的應(yīng)用實例。本文是基于上述思路進行研究工作的,工作主要如下:(1)針對目前動態(tài)描述邏輯的判斷算法不支持一般概念包含公理的現(xiàn)狀,首先,將描述邏輯DL-Lite、動態(tài)邏輯和動作理論結(jié)合,并限制涉及到角色的包含斷言中不能出現(xiàn)否定,構(gòu)建出了新的動態(tài)描述邏輯R prDDL-Lite;然后,給出了其語法與語義,以及為其設(shè)計了Tableau算法并介紹算法的整個過程;最后,對其可終止性、可靠性與完備性進行了分析與證明。(2)為了更好的應(yīng)用于實際問題當中,需要對R prDDL-Lite公式的可滿足性問題進行快速簡便的判定。因此,在上述R prDDL-Lite的算法基礎(chǔ)上開發(fā)出相對應(yīng)的R prDDL-Lite(Tableau)推理機軟件,介紹了軟件的功能、設(shè)計與工具演示,讓使用者更容易理解與使用。(3)語義Web下知識庫是不斷演化的,類比數(shù)據(jù)庫,基于描述邏輯DL-Lite的知識庫也同樣面臨著事務(wù)回滾和事務(wù)并發(fā)的問題,于是在R prDDL-Lite的基礎(chǔ)上引入逆動作和并發(fā)動作,構(gòu)建了支持逆動作和并發(fā)動作的動態(tài)描述邏輯R prCDDL-Lite,研究其在DL-Lite知識庫動態(tài)演化中的應(yīng)用。
【關(guān)鍵詞】：描述邏輯 動態(tài)描述邏輯 可滿足性問題 Tableau算法 事務(wù)
【學(xué)位授予單位】：桂林電子科技大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2015
【分類號】：TP393.09
【目錄】：

• 摘要3-4
• ABSTRACT4-9
• 第一章 緒論9-16
• 1.1 研究背景及意義9-11
• 1.2 國內(nèi)外研究現(xiàn)狀11-14
• 1.2.1 描述邏輯11
• 1.2.2 動作理論11-12
• 1.2.3 描述邏輯的動態(tài)擴展12-13
• 1.2.4 語義Web、知識庫與數(shù)據(jù)庫13-14
• 1.3 研究內(nèi)容14
• 1.4 論文結(jié)構(gòu)14-16
• 第二章 相關(guān)基礎(chǔ)知識介紹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 動態(tài)描述邏輯D-ALCO18-20
• 2.2.1 動態(tài)描述邏輯概述18
• 2.2.2 動態(tài)描述邏輯D-ALCO的語法18-19
• 2.2.3 動態(tài)描述邏輯D-ALCO的語義19-20
• 2.3 相關(guān)推理問題20-22
• 2.3.1 引言20
• 2.3.2 Tableau概述20-21
• 2.3.3 描述邏輯DL-Lite的Tableau判定算法21
• 2.3.4 動態(tài)描述邏輯D-ALCO的Tableau判定算法21-22
• 2.4 語義Web、知識庫與數(shù)據(jù)庫相關(guān)知識22-24
• 2.4.1 語義Web22-23
• 2.4.2 知識庫與數(shù)據(jù)庫的比較23-24
• 2.5 本章小結(jié)24-25
• 第三章 動態(tài)描述邏輯prRDDL-Lite及其可滿足性判定算法25-41
• 3.1 引言25
• 3.2 動態(tài)描述邏輯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 算法預(yù)處理28-29
• 3.3.2 算法詳細過程29-32
• 3.4 prRDDL - Lite的Tableau判定算法的性質(zhì)32-38
• 3.4.1 算法的可終止性32-34
• 3.4.2 算法的可靠性和完備性34-38
• 3.5 prRDDL - Lite公式的判定過程實例38-40
• 3.5.1 判定結(jié)果為可滿足的實例38-39
• 3.5.2 判定結(jié)果為不可滿足的實例39-40
• 3.6 本章小結(jié)40-41
• 第四章 推理機軟件的設(shè)計與實現(xiàn)41-51
• 4.1 引言41
• 4.2 系統(tǒng)設(shè)計與實現(xiàn)41-45
• 4.2.1 開發(fā)環(huán)境41
• 4.2.2 系統(tǒng)功能41-43
• 4.2.3 系統(tǒng)框架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 結(jié)果顯示面板49-50
• 4.4 本章小結(jié)50-51
• 第五章 動態(tài)描述邏輯prRCDDL-Lite及其可滿足性判定算法51-62
• 5.1 引言51
• 5.2 動態(tài)描述邏輯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 算法預(yù)處理54
• 5.3.2 算法詳細過程54-55
• 5.4 prRCDDL - Lite公式的判定過程實例55-58
• 5.4.1 判定結(jié)果為可滿足的實例55-57
• 5.4.2 判定結(jié)果為不可滿足的實例57-58
• 5.5 prRCDDL - Lite的Tableau判定算法的性質(zhì)58-59
• 5.6 prRCDDL - Lite在DL-Lite知識庫動態(tài)演化中的應(yīng)用研究59-61
• 5.6.1 事務(wù)的概念59
• 5.6.2 事務(wù)的prRCDDL - Lite表示59-61
• 5.7 本章小結(jié)61-62
• 第六章 結(jié)束語62-64
• 6.1 主要研究工作總結(jié)62
• 6.2 研究展望62-64
• 參考文獻64-68
• 致謝68-69
• 攻讀碩士學(xué)位期間發(fā)表或錄用的論文69

【參考文獻】

中國期刊全文數(shù)據(jù)庫 前2條

1 梅婧;林作銓;;從ALC到SHOQ(D):描述邏輯及其Tableau算法[J];計算機科學(xué);2005年03期

2 孟小峰,周龍驤,王珊;數(shù)據(jù)庫技術(shù)發(fā)展趨勢[J];軟件學(xué)報;2004年12期

，

本文編號：779790