描述逻辑FLε合一算法

刘 凯

（辽宁师范大学数学学院 辽宁 大连 116029）

0 引言

描述逻辑是一种基于对象的知识表示的形式化，也叫概念表示语言或术语逻辑，一个描述逻辑系统包含四个基本组成部分：表示概念和关系的构造集；TBox包含断言；ABox实例断言；TBox和ABox上的推理机制。它们能够被用作表示在结构上和形式上为人所熟知的方法的应有领域中的概念知识。它们应用于各种各样的应用领域，例如：自然语言，组态，数据库和本体[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而被做成相等。这导出我们的概念项的合一算法，也就是，两个概念项通过应用一个适当的替代，其中替代通过概念项取代概念名。

1 FLε的合一算法

首先我们定义FLε-概念项及这些项的包含和相等关系的语法和语义。FLε的用通常的方法来定义，应用一个解释I=（DI，·I）的概念，且存在一个非空领域DI和一个解释函数·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是出现在Γ中的变量集，σ，θ是这个问题的两个合一算子。我们定义σ≤·θ当且仅当有一个替代λ，对于所有的X∈V使得 θ（X）=λ（σ（X））。

如果σ≤·θ，那么我们说θ是σ的一个例子。

定义2 令Γ是一个FLε-合一算法问题，替代集M被叫做Γ的一个完备合一算子集当且仅当它满足接下来的两个性质：

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

2.如果θ是Γ的一个合一算子，那么存在一个合一算子σ∈M，使得σ≤·θ。这个集合M被叫做Γ的一个最小合一算子集，当且仅当它额外地满足

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

定义3 令Γ是一个FLε-合一算法问题。这个问题有单一的类型（有限的，无限的）当且仅当它有一个最小完备合一算子集基数1（有限基数，无限基数）。如果Γ没有一个最小完备合一算子集，那么它是零型。

2 FLε的相等和包含

为了能够特征化FLε-概念项的相等，一个简化的FLε-概念项在[17]被引入，一个给定的FLε-概念项能通过应用合取的交换和结合模态的如下规则转化成一个相等的简化项。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ε-合一算法的可判定的证明中，我们将利用这个事实严格包含的你顺序是有充分根据的。

命题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的出现，如果C′通过用D′取代所有D的出现从C 中获得，那么 C＞isC′。

命题2 令Γ是一个FLε-合一问题。那么Γ是可解的当且仅当它有一个最小的简化的基合一算子。

引理3 令Γ是一个FLε-合一问题，且γ是一个最小的简化基算子。如果C是γ的 一个原子，那么有Γ的一个非变量原子D，使得C≡γ（D）。

命题3 令Γ是一个平坦的FLε-合一问题且γ是Γ的一个最小的简化基算子。如果X是出现在Γ中的一个概念变量，那么γ（X）≡T或者有一个 Γ 的非变量原子 D1，…，Dn（n≥1）使得 γ（X）≡γ（D1）∩…∩γ（Dn）。

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

5 结论

本文分析了描述逻辑合一算法的研究进展和存在问题，在Badder F的基础上又进一步研究了带存在和任意算子的描述逻辑FLε的合一算法问题。给出了FLε的合一算法的定义，我们已经证明在DLFLε的合一算法是零型和其中的εL-合一算法是非决定性多项式完全（NP-complete）。

模态逻辑和描述逻辑有一个紧密的联系是众所周知的。例如这个DLALC，它能向FLε加入否定来获得，对应于基本的（多）模态逻辑K，在K中的合一算法的判定是一个长期存在的开问题。最近，在K-一些扩展（例如，通过一元模态）的合一算法不可判定已经被证明，子布尔模态逻辑的合一算法（也即是，模态逻辑在所有布尔操作符下不闭，正如FLε的模态逻辑相等），据我们所知，模态知识中没有被考虑。

［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].