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

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

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

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

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

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

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

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

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

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

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