IS-εL系統(tǒng)循環(huán)定義術語集的可滿足性推理.pdf

1、描述邏輯（DLS)是一類知識表示的形式系統(tǒng)，其以結構化、形式化的方法定義應用領域的概念及刻畫領域內(nèi)的信息.描述邏輯具有強大的表達能力、有效推理等優(yōu)點，它的核心是推理服務.一直以來描述邏輯受到人們的關注，描述邏輯在信息系統(tǒng)軟件工程以及自然語言處理等領域得到了廣泛的應用.特別是在第三代Web-語義網(wǎng)中扮演者關鍵角色，并成為W3C推薦Web本體語言OWL的邏輯基礎.
　　Nebel率先深入研究描述邏輯循環(huán)定義，提出循環(huán)定義的3種語義.接

2、著F.Baader建立語法描述圖GT和語義描述圖GJ,使用描述圖及圖之間的模擬關系給出描述邏輯系統(tǒng)εL在循環(huán)定義下3中語義的被定義概念的可滿足性推理和包含關系推理算法，并證明推理算法是多項式時間復雜的.
　　隨著研究工作的深入，人們不滿足于只帶交算子和全稱算子的描述邏輯系統(tǒng)FL0和只帶交算子和存在算子的描述邏輯系統(tǒng)εL的表達力，許多人們在已有研究基礎上通過增加構造子等方式繼續(xù)研究.在此基礎上，本文初步探討增加角色的逆算子，角色的合

3、成算子的描述邏輯系統(tǒng)IS-εL循環(huán)定義術語集的可滿足性推理.本文并不針對F.Baader中循環(huán)定義的3種語義的某一種語義討論，即不設定特定語義環(huán)境討論可滿足性.因為不管是在哪種語義下的可滿足性，只要被定義概念是是有解的，那么其可滿足.以Baader的結論1為起點，在最大不動點語義下，一個待定義的概念A∈Ndef是否可滿足（在給定的基解釋（△，J)中）要求的條件:存在一個語法描述圖GT到語義描述圖GJ的一個模擬:GT(≒)GJ該結論較一般

4、化，具有概括性，也可以理解為要求的條件苛刻.本文認為該結論是一個抽象的一般化的結論，所以嘗試從細節(jié)方面探討，針對5個具體的循環(huán)定義依據(jù)其語法圖和語義圖采用路徑匹配的方法判斷其可滿足性，繼而抽象得出一般化的結論.也就是該5個循環(huán)定義有解的必要條件是:語義路徑存在循環(huán).5個循環(huán)定義有解的充要條件是:存在尾部循環(huán)的語義路徑圖使得語法路徑圖與之匹配，并且尾部循環(huán)的語義路徑圖上的結點就是被定義概念的解.使用路徑圖之間的匹配關系給出該5種被定義概念

5、在IS-εL循環(huán)術語集的可滿足性推理算法，并證明了推理算法是多項式時間復雜的.這樣如果存在特定的語義路徑圖，則可以快速判斷該路徑上的結點是否是被定義概念的解.這樣的結論是具有意義的.前人判斷某元素是否是解的方法一般有:把某元素放到被定義式中驗證看其是否滿足左右的定義式或者根據(jù)在最大不動點語義下，根據(jù)Baader的結論1的方法尋找是否存在一個GT到GJ的一個模擬.不管怎樣，這兩種方法的共同特點在于:每個可能是解的元素都要一一驗證.這對于計

6、算機判斷中是不夠快速有效的.關于本文中判斷是解結論中是根據(jù)特定的語義路徑圖的形狀來判定的，并且得到的往往是一群相關元素是否是解的問題.如果把特定形狀的語義路徑圖存儲在計算機中再匹配，毫無疑問這樣的匹配是快速有效率的，不需一一驗證，可以節(jié)省更多時間和空間.
　　本文主要工作如下:
　　第二章，介紹了描述邏輯系統(tǒng)IS-εL的語法及語義等預備知識.
　　第三章，介紹描述圖.
　　第四章，引入路徑匹配的方法判斷循環(huán)定義的

7、可滿足性.
　　本文的主要研究成果總結如下:
　　命題10N≡(3)r.N.其中α1∈GT,α2∈GJ.
　　若α2是一個由某x開始的復合路徑，它的每一條邊都是r.而且，每一單路徑都以循環(huán)為尾部.令S={x|x是α2的結點元素}，N=S(C)△J,則以下3個結論成立:
　　1.α1與α2匹配;
　　2.S={x|x是α2的結點元素}.則N=S(C)△J是N≡(3)r.N的解;
　　3.結論1與結論2等

8、價.
　　命題14 N=(3)r1.N(∏)(3)r2.N.
　　α2∈GJ，若α2是由某x開始的復合路徑，該路徑上的每個結點分別存在r1，r2的邊.而且，每一單路徑都以循環(huán)為尾部.令S={x;x是α2的結點元素}，N=S(C)△J,則以下3個結論成立:
　　1.α1與α2匹配;
　　2.S={x|x是α2的結點元素}.則N=S(C)△J是N≡(3)r1.N(∏)(3)r2.N的解;
　　3.結論1與結論3

9、等價.
　　命題16 N≡(3)r1.N1，N1≡(3)r2.N.
　　α2∈GJ,α2是一個由某元素x開始的復合路徑，它是以r1，r2（以r1或者r2開始）交替為邊的多個起點的路徑，而且，每一單路徑都以循環(huán)為尾部.令S1={x|(3)y，(3)z，(x,y)∈r1∧(y，z)∈r2，x是α2的結點元素}，S2={x|(3)y，(3)z，(x，y)∈r2∧(y，z）∈r2，x是α2的結點元素}，S=S1∪S2={x|x是α2

10、的結點元素}，N=S1(C)△J, N=S2(C)△J,則以下3個結論成立:
　　1.α1與α2匹配;
　　2.N=S1(C)△J，N1=S2(C)△J分別是N≡(3)r1.N1，N1≡(3)r1.N的解;
　　3.結論1與結論2等價.
　　命題19給定描述邏輯IS-εL的TBoxT是N≡(3)r.N，J1=（△J1，·J1），J2=（△J2，·J2）是兩個不同的基解釋.語法圖GT=(Ndef, ET, LT)，