本文關(guān)鍵詞：描述邏輯FLε的合一算法，由筆耕文化傳播整理發(fā)布。

描述邏輯FLε合一算法

【摘 要】描述邏輯（DL）一族知識(shí)表示系統(tǒng)，是一個(gè)非常熱門的研究方向。一方面，重要的推理問(wèn)題如包含問(wèn)題是多項(xiàng)式得；另一方面，F(xiàn)Lε被用做定義大的本體。已經(jīng)提出的描述邏輯的合一算法能夠作為一個(gè)新奇的推理服務(wù)，它被用做發(fā)現(xiàn)本體的冗余。本文主要的結(jié)果是FLε合一算法是可判定的。更精確地，，F(xiàn)Lε的一個(gè)部分εL是多項(xiàng)式完全，因此它和εL匹配有相同的計(jì)算復(fù)雜性。本文首先給出了描述邏輯系統(tǒng)FLε的語(yǔ)法和語(yǔ)義，特別地，蘊(yùn)含合一問(wèn)題沒(méi)有有限的完備合一算子集，基于合一算法的規(guī)則探討了可判定性問(wèn)題。

【關(guān)鍵詞】描述邏輯；FLε；合一算法；合一類型；可判定性

0 引言

描述邏輯是一種基于對(duì)象的知識(shí)表示的形式化，也叫概念表示語(yǔ)言或術(shù)語(yǔ)邏輯，一個(gè)描述邏輯系統(tǒng)包含四個(gè)基本組成部分：表示概念和關(guān)系的構(gòu)造集；TBox包含斷言；ABox實(shí)例斷言；TBox和ABox上的推理機(jī)制。它們能夠被用作表示在結(jié)構(gòu)上和形式上為人所熟知的方法的應(yīng)有領(lǐng)域中的概念知識(shí)。它們應(yīng)用于各種各樣的應(yīng)用領(lǐng)域，例如：自然語(yǔ)言，組態(tài)，數(shù)據(jù)庫(kù)和本體[1]。

兩個(gè)項(xiàng)？坌child.Rich∩？坌child.Woman和？坌child.（Rich∩Woman）是相等的，如果我們用存在限制符（？堝r.C）取代值限算子符，那么這個(gè)等式不再成立。然而，？堝child.Rich∩？堝child.（Woman∩Rich）≡？堝child.（Woman∩Rich）通過(guò)用項(xiàng)Female∩Human取代Woman，這個(gè)概念項(xiàng)Woman∩？堝child.Woman和Female∩Human∩？堝child.（Female∩Human）是不相等的，但是它們意味著表示相同的概念。這兩個(gè)項(xiàng)明顯地能通過(guò)概念項(xiàng)Female∩Human替代第一個(gè)項(xiàng)中的概念名Woman而被做成相等。這導(dǎo)出我們的概念項(xiàng)的合一算法，也就是，兩個(gè)概念項(xiàng)通過(guò)應(yīng)用一個(gè)適當(dāng)?shù)奶娲渲刑娲ㄟ^(guò)概念項(xiàng)取代概念名。

1 FLε的合一算法

5 結(jié)論

本文分析了描述邏輯合一算法的研究進(jìn)展和存在問(wèn)題，在Badder F 的基礎(chǔ)上又進(jìn)一步研究了帶存在和任意算子的描述邏輯FLε的合一算法問(wèn)題。給出了FLε的合一算法的定義，我們已經(jīng)證明在DL FLε的合一算法是零型和其中的εL-合一算法是非決定性多項(xiàng)式完全（NP- complete）。

模態(tài)邏輯和描述邏輯有一個(gè)緊密的聯(lián)系是眾所周知的。例如這個(gè)DL ALC，它能向FLε加入否定來(lái)獲得，對(duì)應(yīng)于基本的（多）模態(tài)邏輯K，在K中的合一算法的判定是一個(gè)長(zhǎng)期存在的開問(wèn)題。最近，在K-一些擴(kuò)展（例如，通過(guò)一元模態(tài)）的合一算法不可判定已經(jīng)被證明，子布爾模態(tài)邏輯的合一算法（也即是，

  本文關(guān)鍵詞：描述邏輯FLε的合一算法，由筆耕文化傳播整理發(fā)布。