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

描述邏輯FLε合一算法

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

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

0 引言

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

兩個項？坌child.Rich∩？坌child.Woman和？坌child.（Rich∩Woman）是相等的，如果我們用存在限制符（？堝r.C）取代值限算子符，那么這個等式不再成立。然而，？堝child.Rich∩？堝child.（Woman∩Rich）≡？堝child.（Woman∩Rich）通過用項Female∩Human取代Woman，這個概念項Woman∩？堝child.Woman和Female∩Human∩？堝child.（Female∩Human）是不相等的，但是它們意味著表示相同的概念。這兩個項明顯地能通過概念項Female∩Human替代第一個項中的概念名Woman而被做成相等。這導出我們的概念項的合一算法，也就是，兩個概念項通過應用一個適當?shù)奶娲�，其中替代通過概念項取代概念名。

1 FLε的合一算法

5 結論

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

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

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