公理定位是本体调试的一个重要环节,目前主要分为两类:最大可满足子术语集(A-MSSs,Maximally A-satisfiable subsets),最小不可满足保持子术语集(MUPS,Minimal unsatisfiability preserving sub-TBox)或者辩护(justification),其中辩护是比MUPS广泛的概念。关于A-MSSs,主要是Meyer^{[ 1]}针对非展开ALC本体,提出一种基于tableau演算的方法计算最大可满足子术语集,给出相应的优化技术。关于MUPS,Schlobach^{[ 2, 3]}提出自上而下计算不可满足概念的所有MUPS方法(针对非展开ALC本体)和自底向上计算一个MUPS方法。关于justification,Kalyanpur^{[ 4, 5]}对同一本体中多个不可满足概念之间的关联性做了分析和研究,定义了不可满足概念的依赖,结合碰集方法只对一些特殊概念计算其辩护(等价于Schlobach提出的MUPS)。此外,Baader^{[ 6]}证明了基于自动机的DLs推理方法可以被扩展到本体调试的定位,即一个单调布尔公式的最小值MUPS(或者辩护)对应。本体调试的另一个重点是对故障知识库的诊断。诊断是调试的一个重要部分,集中于识别导致本体不一致的公理集。Schlobach^{[ 7]}提出了本体术语集的调试框架,以传统的模型诊断为基础^{[ 8, 9]}。Friedrich^{[ 10]}给出本体中诊断的一般概念,并提供正确完备的计算极小诊断的方法。Shchekotykhin^{[ 11]}通过对目标本体进行查询确定最终的目标诊断。处理本体不一致的方法有很多,Haase和Qi^{[ 12]}对本体调试研究进行系统性的分析和综述,得出结论:没有哪一种本体调试的方法是普遍适用于所有应用场景的,不同的方法是适合于不同调试目的和调试要求的。

在本体语境下,概念的定义方式直接影响概念的可满足性,由于公理描述中使用的概念相互矛盾,从而导致公理所定义的概念不可满足。这样,结合模型诊断,不可满足概念对应的公理被认为是故障部件,我们要解决的问题就是在本体术语集的局部(即故障部件内部)定位冲突概念。为了实现这种局部定位逻辑错误,首先需要将故障部件转换成等价的系统模型即部件术语集,二者具有相同的输入和输出,并且在相同的输入值下得到相同的输出值,然后以系统中剩余的部件为基础,在该子系统中进行局部查找极小冲突集,即MUCS。本文研究只有包含公理(概念和角色包含公理)的本体术语集,对于等价公理,需要将其转换成相应的包含公理。

2.1 基于诊断的部件术语集

部件术语集的转化规则如下:

The → -rule^R

If Γ contains C'⊆C₁∩C₂,but it does not contain both C'⊆C₁ and C'⊆C₂.

Then Γ=Γ\{C'⊆C₁∩C₂}∪{C'⊆C₁,C'⊆C₂}.

The→ -rule^R

If Γ contains C'⊆C₁∪C₂, and either C₁ or C₂ is not A,﹁A,μ.A or μ.¬A where A is an atomic concept or T and μ is $R,∀R,≥nR or ≤nR.

Then Γ=Γ\{C'⊆C₁∪C₂}∪{C'⊆C'₁∪C'₂,C'₁⊆C₁,C'₂⊆C₂} where C'₁ and C'₂ are new concepts not occurring in T and Γ.

The →_λ-rule^R

If Γ contains C'⊆λ.D where λ is $R, ≥nR or ≤nR and n is a non-negative integer.

Condition: D is D₁∩D₂, then Γ=Γ\{C'⊆λ.D}∪{C'⊆λ.D',D'⊆D₁,D'⊆D₂};

Condition:D is D₁∩D₂,then Γ=Γ\{C'⊆λ.D}∪{C'⊆λ.D₁⊆λ.D₂};

where D' is a new concept not occurring in T and Γ.

The →_∀-rule^R

If Γ contains C'⊆∀R.D.

Condition: D is D₁∩D₂, then Γ=Γ\{C'⊆∀R.D}∪{C'⊆∀R.D₁,C'⊆∀R.D₂};

Condition: D is D₁∪D₂ and either D₁or D₂ is not A,﹁A, μ.A or μ.﹁A where A is an atomic concept or T and μ is ∃R,∀R, ≥nR or ≤nR, then Γ=Γ\{C'⊆∀R.D}∪{C'⊆▯R.(D₁'∪D₂'), D₁'⊆D₁, D₂'⊆D₂};

where D₁' and D₂' are new concepts not occurring in T and T.

给定TBox T,α_C是T中概念C的定义公理,假设α_C的右边概念是否定标准形式(¬只出现在原子概念的前边)。为了计算α_C对应的术语集,该算法由TBox Γ={α_C}开始,对Γ应用规则,直到没有规则可用时终止,称最后得到的Γ为α_C的部件术语集(Component terminology)。

结论1 设α是TBox T中概念C的定义公理,Γ是把转换规则应用于{α}得到的术语集,那么,C基于T\{α}∪Γ是不可满足,的当且仅当C在T下不可满足。

我们将公理α的部件术语集记作Γ_α,同样地,内部的每条公理是系统Γ_α的一个部件。根据部件术语集的计算规则,不难知道α的模型也是Γ_α的模型,同时α的模型可以通过扩展Γ_α的模型得到。另外,按照给出的规则,可以得到唯一确定的公理的部件术语集。

图1

Fig.1

	Figure Option ViewDownloadNew Window
	图1 本体术语集对应的模型诊断系统图Fig.1 Model-Based Diagnosis system for terminologies

图1中,上边部分是TBox T={ β₁, β₂, β₃}对应的系统(输入为基本概念 A和 B),观测为 T不一致,并且 C₃是不可满足的,对 T进行诊断得到 M={ β₁, β₂, β₃}是系统 T的极小冲突集;下边部分 Γ={ β₃₁, β₃₂, β33}是 T中公理 β₃对应的系统,即部件术语集(输入是 C₁、 C₂和 D, Γ与 T中部件 β₃具有相同的输入和输出(值)),得到新的本体术语集 T'=T∪ Γ, M'={ β₁, β₂, β31, β32}是系统 T'的极小冲突集,将 M'对应到 M,{ β₃₁, β₃₂}是故障部件 β₃的具体定位,同时说明 C₃的可满足性与 D无关。

例子TBox T₁中 α₁和 α₆的部件术语集分别为 Γ_α1 ={ A₁⊆ ¬A, A₁⊆ A₂, A₁⊆ A₃}, Γ_α6 ={ A₆⊆ A₁∪ X₁, X₁⊆ $r.X₂, X₂⊆ A₄, X₂⊆ ¬C, X₂⊆ A₃}。

本节给出计算不可满足概念单个MUCS的黑盒方法,进一步地结合Retiter的碰集自上而下地计算所有MUCS。算法与DL推理机相互独立,需要推理机提供概念在相应的本体下可满足性测试结果,而推理机内部的具体实现对算法是不可见的。通过调用外部DL推理机,实现对任意基于DL语言的本体进行调试。其中,如果概念不止一条定义公理,那么,将合并每条定义公理的部件术语集,合并结果作为概念的定义公理的部件术语集。

Algorithm SINGLE_MUCS(T,C,S_c)

Input: TBox T, Concept C, subset of component terminology of Cs axioms S_c

Output: set of axioms M

M ← Æ

T₁←S_c∪(T-{α_c|α_c is the axiom of C in T})

if C is satisfiable w.r.t T₁,then

return Æ

for each axiom α∈S_c,do

T₁←T₁-{α}

if C is satisfiable w.r.t T₁,then

M←M∪{α}

T₁←T₁∪{α}

return M

SINGLE_MUCS算法实现求解TBox T中不可满足概念 C在公理集 T'∪ S_c下的一个MUCS,其中 S_c是 C的定义公理的部件子术语集(部件术语集的子集), T'为 T除去 C的定义公理之后的本体术语集。如果 C在 T'∪ S_c是可满足的,返回值为空;否则,逐个处理 S_c中的公理。删除 S_c中的公理 α之后,若 C仍是不可满足的,说明删除的公理不影响 C在 T'∪ S_c中的可满足性, α不是 C的不可满足的逻辑错误;若 C是可满足的,则 α是 C的逻辑错误原因,将其保存到 M中,同时将 α恢复到本体中,其中 M是最后的返回结果。

定理1 C是TBox T中一个不可满足概念,如果 C在 T'∪ S_c下是不可满足的,那么SINGLE_MUCS( T, C, S_c)∈ mucs( T, C),其中 S_c是 C的定义公理的部件子术语集, T'为 T除去 C的定义公理之后的本体术语集。

证明 TBox T中不可满足概念 C在 T'∪ S_c下是不可满足的,SINGLE_MUCS算法中变量 M就是 C的一个MUCS。循环处理 S_c中公理之前设 S_c={ α₁,…, α_m}。 ①首先, C在 T'∪ M下是不可满足的。本体逐个删除 S_c中公理 α_i(1≤ i≤ m),如果 C可满足,则将所删除公理恢复到本体同时保存到 M中,否则不做任何操作。这样,删除 α_i之前, C在当前本体 T'∪ M∪{ α_i,…, α_m}下是不可满足的,处理完 S_c中所有公理之后, C在 T∪ M下是不可满足的。 ②任意 M'⊂ M, C在 T'∪ M'下是可满足的。假设存在 M'⊂ M使得 C在 T'∪ M'下不可满足,令 D_c=M-M',那么对任意 M″⊂ M'都有 C在 T'∪ M″下是不可满足的。处理完 S_c-D_c中所有公理时有 C在 T'∪ M'∪ D_c是不可满足的,当处理 D_c中的公理时都有 C是不可满足的,最后得到的 M=M',这与 M'⊂ M矛盾,假设不成立。证毕。

定理1保证了SINGLE_MUCS算法的正确性和完备性,算法中进行概念可满足性测试与输入参数中部件子术语集 S_c的大小有关,如果 S_c有 n个元素,则最多需要进行 n+1概念可满足性测试。

MUCS_HST是计算不可满足概念所有MUCS的一种黑盒算法,该算法利用Reiter的碰集树方法,对SINGLE_MUCS算法得到的单个MUCS进行展开,进而得到概念其他的MUCS。下面首先给出碰集和碰集树的定义。

定义6(碰集^{[ 8]}) 设 F是一个集合簇, F的碰集(hitting set)是一个集合 H⊆∪ _{s∈ F}S,使得对所有 S∈ F, H∩ S≠ Æ。称 F的一个碰集为极小的当且仅当它的任何一个真子集都不是 F的碰集。

定义7(碰集树,HS-tree^{[ 8]}) 设 F是一个集合簇,一个对结点和边做了标记的树 T_r称作是 F的碰集树(HS-tree)当且仅当 T_r满足下列性质:

(1)如果 F为空,则根结点标识为 '√ ';否则,生成作为树根的结点,结点标识为 F中的一个元素。

(2)设 n是 T_r的一个结点,处理结点 n:

①定义 P( n)为从根结点到 n路径上边标识的集合;

②若存在集合 S∈ F使得 S∩ P( n) =Æ,则 n被标识为 S即 L( n) =S,否则,标识为'√';

③若 n被标识为 '√ ',则 n没有后继结点;

④若 n被标识为集合簇 F的一个集合 Σ,则对每一个 δ∈ Σ, n有一个后继结点 m与 n通过一条边 e=<n, m>相连,边 e的标识为 δ即 L( e) =δ;

如果 n是一个标识为 '√ '的结点,那么 P( n)是 F的一个碰集。 F的每一个极小碰集都是HS-tree中某标识为'√'的结点 n的 P( n)。标识为 '√ '的结点 n的 P( n)并不包含 F的所有碰集,但包含了 F的所有极小碰集。访问 F的意思是为了选择此树中结点的标识所进行的计算,这种选择结点 n的标识的计算是在 F中搜索满足 S∩ P( n) =Æ的集合 S。如果 S被找到,结点 n被标识为 S,否则它被标识为'√'。本文MUCS_HST算法中, F是不可满足概念的所有MUCS,但是 F不是显式地可以获得的,一次对 F的访问需要调用SINGLE_MUCS计算 F的一个MUCS。为了产生一棵尽量小、只给出 F的极小碰集、访问 F次数最少的HS-tree,在BUILD_HST算法生成碰集树的过程中:①采用宽度优先来扩展结点;②关闭规则:如果结点 n已被标识为 '√ ',且新结点 n'满足: P( n) ÍP( n'),那么可以关闭 n'( L( n) ='×')不对 n'继续扩展; ③重用结点规则:设结点 n被∑标识出( Σ={ δ,…}),若碰集树中存在 n',使得 L( n')∩( P( n)∪{ δ}) =Æ,那么让 n下的 δ-弧指向这个已经存在的 n',不需要再扩展 n',否则调用SINGLE_MUCS产生新结点并对新结点进行扩展。

MUCS_HST算法中,变量 HS保存碰集, F保存得到的MUCS。算法首先为构造的碰集树提供一个根结点 r,并将 r加入到队列QUEUE中,然后逐个扩展QUEUE中结点。这样,以队列的方式实现宽度优先遍历,对每个结点进行完全展开生成碰集树。碰集树中除了标识为'√'和'×'的结点,剩余的结点都是相应不可满足概念的MUCS,并且是所有的MUCS。

定理2 C是TBox T中一个不可满足概念, α是 C在 T中的定义公理, T_c =T\{ α}∪Γ _α。 C基于 T'⊂ T_c是可满足的当且仅当 H=T_c -T'是 mucs( T_c, C)的一个碰集, H是 mucs( T_c, C)的极小碰集当且仅当对任意 H'⊂ H, C基于 T_c -H'是不可满足的。

定理3 如果 T_r是MUCS_HST( T, C)算法生成的碰集树,那么下列两个命题等价:

(1)令 N( T_r)为碰集树 T_r中所有标识为 '√ '的叶结点 n的集合, M( T)为 mucs( T, C)所有极小碰集的集合,那么 ∪_n∈N(Tr) P( n) =M( T);

(2)MUCS_HST( T, C)= mucs( T, C);

定理2和3的正确性都可以根据Reiter的碰集树理论得到证明,这里证明略。

MUCS_HST( TC)算法如下

Algorithm MUCS_HST(T,C)

Input:TBox T, Concept C

Output:set of axiom sets S

get the defining axiom α of C in T

S_c←T_α

T' ←T \ {α}∪S_c

m ← SINGLE_MUCS(T', C, S_c)

create a node r and set L(r) ← m

HS ← Æ

F ← {m}

QUEUE ← {r}

while QUEUE is not empty, do

N ← get the head element of QUEUE

for each axiom β∈L(N), do

create a new node N' and set L(N')←Æ

create a new edge e=<N, N'> with L(e)←β

if there exists a set hÎHS s.t. hÍP(N)∪{β},then

L(N') ←'×'

else if there exists a set k∈F s.t. k∩(P(N)∪{β})=Æ,

then

L(N')←k

QUEUE←QUEUE+N'

else

A_c←S_c-P(N)-{β}

m ←SINGLE_MUCS(T, C, A_c)

if m = Æ, then

L(N')←'√'

HS←HS∪{P(N)∪{β}}

then

L(N') ←m

F ← F∪{m}

QUEUE ←QUEUE + N'

return F

本文实验是在PC机win7操作系统(Intel(R) Core(TM)i5-3470 CPU @3.20 GHz,8.00 GB的内存)下运行,前边描述的算法都用java语言实现,调用pellet推理机判断概念的可满足性。通过实验说明计算不可满足概念的MUCS实现本体调试的可行性,基本测试方法是用现实本体检测调试方法性能。由于现实中可用的不一致本体术语集有限,本文采用Koala本体和DICE本体的一个片段对本文调试方法进行评估。MadCow是ALCH(D)本体,包括53个概念1个不可满足概念和41条公理,本文方法所需时间为15 ms;DICE是ALCH本体,其中包含527个概念、76个不可满足概念和505条公理,本文方法所需时间为23.151 s。

Case 1:mad+cow是MadCow本体中一个不可满足概念.

α₁: mad+cow⊆cow∩$eats.(brain ∩$part+of.sheep)

α₂: cow⊆vegetarian

α₃: vegetarian ⊆∀eats.∀part+of.﹁ animal∩ animal ∩∀eats.﹁ animal

α₄: sheep ⊆∀eats.grass∩ animal

mups(MadCow, mad+cow)={{α₁,α₂,α₃,α₄}}

mucs(MadCow,mad+cow)={mad+cow⊆cow,mad+cow⊆X₁, X₁⊆$eats.X₂,X₂⊆$part+of.sheep}

Case 2:B292是DICE本体中一个不可满足概念.

β₁: B292 ⊆C151∩L12∩…(其中,省略号部分表示有近百个原子概念否定的合取)

β₂: C151⊆Z141∩…

β₃: L12 ⊆﹁ Z141∩…

mups(DICE, B292)={{β₁,β₂,β₃}}

mucs(DICE, B292)={{B292⊆C151, B292⊆L12}}

MUCS能够正确地给出概念不可满足的逻辑错误。MadCow本体中,mad+cow只有一个MUCS即{mad+cow⊆cow,mad+cow⊆X₁,X₁⊆$eats.X₂,X₂⊆$part+of.sheep},说明mad+cow的不可满足错误是由于cow与$eats.$part+of.sheep同时定义mad+cow,从而发生矛盾引起的。消去新增的概念X₁和X₂,得到cow的定义与$eats. $part+of.sheep冲突。这样,MUCS直接将mad+cow的错误定位到$eats.$part+of.sheep,排除$eats.brain。所以,MUCS可以更精确地在公理的内部找到概念不可满足原因的位置。DICE本体中,有一部分不可满足概念的定义公理类似Case 2中的B292的定义形式,每个不可满足概念的定义公理较大(公理中合取构造符的数量为公理的长度)。这种情况下,相较于MUPS,MUCS能更加详细地给出逻辑不一致的原因。

实验证明利用MUCS进行本体调试的可行性,MUCS与MUPS是相互独立的,互不影响,得到的调试结果都能在不同程度上指出本体不一致的位置。不可满足概念的定义公理规模越大,MUCS_HST算法的执行时间越长。

通过对公理进行规则变换得到对应的部件术语集,在此基础上定义不可满足概念的MUCS,MUCS将不可满足概念的逻辑错误更具体地定位到概念定义公理的局部。文中所提出的利用Reiter碰集树方法计算不可满足概念所有MUCS的MUCS_HST算法较好地实现了这一想法。在实验评测环节,采用现实本体对MUCS_HST算法进行实验测试:测试结果表明利用MUCS将不一致本体的逻辑错误定位到公理的局部是可行的,与求解MUPS的现有本体调试相互独立并不冲突;另外,概念的定义公理直接影响算法的执行时间。