描述邏輯FLε合一算法

劉 凱

（遼寧師范大學數(shù)學學院 遼寧 大連 116029）

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ε的合一算法

首先我們定義FLε-概念項及這些項的包含和相等關系的語法和語義。FLε的用通常的方法來定義，應用一個解釋I=（DI，·I）的概念，且存在一個非空領域DI和一個解釋函數(shù)·I能夠分配關于的二元關系到角色名及DI的子集到概念項。正如表1的列所表示的語義。

表1 FLε的語法和語義Tab.1 Syntax and Semantics of FLε

為了定義概念項的合一算法，我們首先引入關于概念項的一個替代操作概念。為了這個目的，我們劃分概念名集到一個概念變量集Nv（它可能被替代所取代）和概念常量集Nc（它一定不能被替代所取代）。一個替代σ是一個從Nv到FLε-概念項集的映射，這個映射在明顯的方式下被擴展到概念項，也就是，-σ（A）:=A，對所有的 A∈Nc，σ（T）:=T，σ（C∩D）:=σ（C）∩σ（D），σ（?r.C）：＝?r.σ（C），且 σ（?r.C）：＝?r.σ（C）。

定義 1 一個 FLε-合一算法問題是形如 Γ＝｛C1≡？D1，…，Cn≡？Dn｝，其中 C1，D1，…，Cn，Dn是 FLε-概念項，這個替代 σ 是 Γ 中一個合一算子（或者解），當且僅當 σ（Ci）≡σ（Di）其中 i=1，…，n，這個例子中，Γ 被叫做可解的或可合一的。

通常情況下，合一算子能用實例前序≤·來比較。令Γ是一個FLε-合一算法問題，V是出現(xiàn)在Γ中的變量集，σ，θ是這個問題的兩個合一算子。我們定義σ≤·θ當且僅當有一個替代λ，對于所有的X∈V使得 θ（X）=λ（σ（X））。

如果σ≤·θ，那么我們說θ是σ的一個例子。

定義2 令Γ是一個FLε-合一算法問題，替代集M被叫做Γ的一個完備合一算子集當且僅當它滿足接下來的兩個性質：

1.M的每一個元素是Γ的一個合一算子；

2.如果θ是Γ的一個合一算子，那么存在一個合一算子σ∈M，使得σ≤·θ。這個集合M被叫做Γ的一個最小合一算子集，當且僅當它額外地滿足

3.如果 σ，θ∈M，那么 σ≤·θ蘊含 σ＝θ。

定義3 令Γ是一個FLε-合一算法問題。這個問題有單一的類型（有限的，無限的）當且僅當它有一個最小完備合一算子集基數(shù)1（有限基數(shù)，無限基數(shù)）。如果Γ沒有一個最小完備合一算子集，那么它是零型。

2 FLε的相等和包含

為了能夠特征化FLε-概念項的相等，一個簡化的FLε-概念項在[17]被引入，一個給定的FLε-概念項能通過應用合取的交換和結合模態(tài)的如下規(guī)則轉化成一個相等的簡化項。C∩T→C，A∩A→A?r.C∩?r.D→?r.C 對所有的 FLε-概念項 C，D 且 C?D

定理1 令C，D是FLε-概念項，且C?，D?是C和D各自簡化形式。那么C≡D當且僅當由∩的結合和交換決定的C?恒等于D?。

引理1 如果 C，D是FLε-概念項的簡化，使得?r.D?C，那么C要么是 T，要么是 C=?r1.C1∩…∩?r.Cn的形式，其中 n≥1；C1，…，Cn是簡化的并且關于包含是成對不可比較的，而且D?C1，…，D?Cn。相反的，如果 C，D 是 FLε-概念項使得 C=?r.C1∩…∩?r.Cn且 D?C1，…，D?Cn，那么?r.D?C。 FLε-合一算法的可判定的證明中，我們將利用這個事實嚴格包含的你順序是有充分根據(jù)的。

命題1 沒有 FLε-概念項的極大結果 C0，C1，C2，C3，…使得 C0?C1?C2?C3?…。

3 一個零型的FLε-合一算法問題

為了證明FLε有合一算法零型，我們展示一個FLε-合一算法問題有這種類型。

定理2 令 X，Y是變量， 這個 FLε-合一算法問題 Γ:＝｛X∩?r.Y≡？?r.Y｝有合一算法零型。

4 可判定性問題

在我們能描述關于FLε-合一算法的可判定程序之前，我們必須引入一些概念。一個FLε-概念項被叫做一個原子當且僅當它是概念名（也即是，概念常量或者概念變量），一個值限?r.D或者一個存在限制?r.D。明顯地，任何FLε-概念項是（等于）原子項的一個合取，其中空合取是T。一個FLε-概念項C的原子集At（C）推導的定義：如果C=T，那么 At（C）:=φ；如果 C 是一個概念名，那么 At（C）:=｛C｝；如果 C=?r.D 那么 At（C）:=｛C｝∪At（D）；如果 C=C1∩C2，那么 At（C）:=At（C1）∪At（C2）。

概念名、值限?r.D和存在限制?r.D其中D是一個概念名或者T被叫做平坦的原子。這個FLε-合一問題Γ是平坦的當且僅當它僅僅包括接下來的形式的方程：-X≡？C其中X是一個變量而C是是非變量的平坦的原子；

-X1∩…∩Xm≡？Y1∩…∩Yn其中 X1，…，Xm，Y1，…，Yn是變量。

引理 2.令 C，D，D′是 FLε-概念項使得 D＞isD′而且 C 是簡化的，并且含有至少一個D的出現(xiàn)，如果C′通過用D′取代所有D的出現(xiàn)從C 中獲得，那么 C＞isC′。

命題2 令Γ是一個FLε-合一問題。那么Γ是可解的當且僅當它有一個最小的簡化的基合一算子。

引理3 令Γ是一個FLε-合一問題，且γ是一個最小的簡化基算子。如果C是γ的 一個原子，那么有Γ的一個非變量原子D，使得C≡γ（D）。

命題3 令Γ是一個平坦的FLε-合一問題且γ是Γ的一個最小的簡化基算子。如果X是出現(xiàn)在Γ中的一個概念變量，那么γ（X）≡T或者有一個 Γ 的非變量原子 D1，…，Dn（n≥1）使得 γ（X）≡γ（D1）∩…∩γ（Dn）。

定理3 εL-合一算法是非決定性多項式完全（NP-Complete）

5 結論

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

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

［1］Baader,F.,Kusters,R.:Matching in description logics with existential restrictions[Z].In:Proc.KR 2000,2000.

［2］Baader,F.,Narendran,P.Unification of concepts terms in description logics[J].J.of Symbolic Computation 31(3),2001.

［3］Badder F,Unification in Commutative Theories[J].J.of Symbolic computation,1989,8(5).

［4］Badder F,Morawska.Unification in the Description logic εL[Z].