第3期 郝国舜，等：一种扩展的动态描述逻辑语言及其Tableau算法 .231. 针对原子模态词m。的规则，每次都把所有.作用 (m.tm)w)Vh的ABox,其中，w=(A,nA,)x), 的断言扩展.因为按照语义定义，这些结果断言应该 =(3R.A)(x),且假设有规约规则：m.4A,几A,口 是属于同一新的可达世界中. 3R.A)x),m(A门A,n3R.A)x)A,门A2U3R.A) 2)+。规则： (x),检查此ABox的协调性. r:m1°m2p 从根节点1(ma°m。,)()V中出发，利用传 o:(m2(m1p) 统描述逻辑的展开规则和本文给出的扩展规则，最 例子1下面通过1个简单的例子，展示 终得到完全展开的Tableau树T,如图2所示.T的 Tableau算法的具体扩展过程.给定包含一个断言 3个叶节点都不包含冲突的，故原ABox协调. 1:(mm中)V门中 1:(m.m。)(中) 1:7 1:m(m。(ψ)》 1:(3R.A)(x) 1.m:m。(A,门A门3R.A(x) 1:R.(7A(x 1.m.m:(d,门1，u3K.A)x) 1:廿R.(1x) 1.m.mn:(A,门4)(x） 1.mm:3R.A,(x) 1:0 1.m。·m:A,(x,A,() 1.m4.mn:R(x,y).A0y） 图2完全展开的Tableau树T' Fig.2 Totally extended Tableau tree T" 3.2 Tableau算法的性质 证明1首先给出断言长度的定义， 下面分析此Tableau算法的性质，证明其具有 定义9（断言长度）任意断言p的长度(p) 可终止性和可靠性 递归定义如下： 3.2.1可终止性 若A是一个原子概念，则(4(x))=1; 显然，把TBox中有限的定义代人到ABox中以 若R是一个角色，则(R(x,y)=1; 消除TBox的过程是可终止的；把ABox中所有断言 若m。是个原子模态词实例，则l(m。)=1, 转化为NNF形式是可终止的；检查完全展开的 l(np）=l(m)+l(), ABox是否存在冲突也是可终止的.因此，Tableau算 l(m1m2）=l(m1)+l(m2）+1. 法可终止性就规约为完全地扩展Tableau树是否可 对于规则→，由于规则中的2个不包含模态词的 终止 断言P、中可能为任意的，因此不能直接考虑其长 定义8(Tableau树展开的可终止性)由某个 度.但此规则的重要性在于消除了1个模态词。， DALC,的ABox为根节点的Tableau树T,不存在无 因此，规则作用前，模态断言的长度为(p)+1,而 限的展开：T+T1→T2→…. 作用后消除了模态词，断言长度为1（中）.因此，其结 对传统描述逻辑的Tableau算法，其可终止性 构长度减少了1.即使每个→%，规则产生的结果断 的证明是通过证明每个扩展规则都减少了断言长 言的绝对长度都增加，即（中）>1（φ），结果断言经 度？9，从而最终把所有断言都扩展成为原子的形 过有限步扩展，还是可以完全展开.因此，此规则的 式，即C(a),C(a),R(a,b)的形式本文算法只是 重要性在于消除了模态词. 增加了对模态词展开规则，因此只对此规则仍然遵 对于规则→o,l(m2(m1p）=l(m1°m2p）-1. 循此长度减少规律做证明。 因此，每个关于模态词的扩展规则使断言长度