第4卷第3期 智能系统学报 Vol.4 No.3 2009年6月 CAAI Transactions on Intelligent Systems Jn.2009 doi:10.3969/j.issn.16734785.2009.03.006 一种扩展的动态描述逻辑语言及其Tableau算法 郝国舜，马世龙，胜跃飞2 (1.北京航空航天大学软件开发环境国家重，点实验室，北京100191：2.中科院计算所智能信息处理重点实验宣，北 京100080) 摘要：对动态系统的描述是智能领域的一个重要问题，但目前已有的动态描述逻辑语言，用不可再分的符号表示 原子动作，不能区分动作类和动作实例，不足以对实际系统中的动作进行表达.因此提出了一个扩展的动态描述逻 辑语言，在原子动作模态词的形式中可以表示动作的属性，从而区分了一类动作和具体动作.通过对可达关系进行 限制，定义了此特殊形式模态词动作的语义.另外，还提供了此语言的Tlu算法，并证明了此算法的可终止性和 完备性. 关键词：动态描述逻辑；模态逻辑；动态逻辑；Tableau算法 中图分类号：TP301文献标识码：A文章编号：16734785(2009)03-0226-08 An extended dynamic description logic language and its Tableau algorithm HAO Guo-shun',MA Shi-long',SUI Yue-fei? (1.National Laboratory of Software Development Environment,Beihang University,Beijing 100191,China;2.Institute of Computing Technology,Chinese Academy of Sciences,Beijing 100080,China) Abstract:Accurate descriptions of actions in a dynamic system are essential,yet dynamic description logic langua- ges presently available cannot meet that need because they use indivisible symbols representing atomic actions.This results in action classes and action instances being indistinguishable,with relationships between different action in- stances similarly inexpressible.An extended dynamic description logic language was proposed by extending the form of atomic modal operators within a parameter set.With the parameter set enabled,an atomic modal operator can re- present a class of actions;by assigning concrete values to a parameter,a sub-class of actions could be generated;a special sub-class of actions containing only one action instance could be generated when all parameters are as- signed.Hierarchy trees of actions could be developed like the concept tree.The action behaviors of the special mo- dal operators were defined in a different manner,not merely two arbitrary possible words but those satisfying certain limitations could be reachable,and the limitations denote action behaviors.Representing actions with hierarchy trees has important meanings in action description.A sound Tableau algorithm was also provided which demon- strates the practical value of the proposed language. Keywords:dynamic description logic;modal logic;dynamic logic;Tableau algorithm 网络环境下的计算，如基于服务的计算，需要计资源时，就要给出服务的语义描述及对语义描述进 算资源的协同合作.这种协同合作在很多方面都表 行推理.语义描述不仅包含静态语义描述，还包括对 现为智能性，如对服务的发现、匹配、组合、调用以及 功能等动态行为的语义描述.因此，对动态系统的描 管理等.这些智能性，建立在对分布计算资源的充分 述及推理，是网络环境下计算的智能性的一个重要 语义描述和自动推理基础之上.比如，服务作为计算 方面.描述逻辑作为可定制，有严格理论基础；并且 作为可自动推理的形式语言，是用来描述资源的理 收疯日期：2008-08-22. 想语言).用描述逻辑语言描述动态的计算系统， 基金项目：国家“973”计划资助项目(2005CB321902) 通信作者：马世龙.E-mail:alma@nlade.buaa.ed加.cm 是网络环境下协同计算的一个基础性工作
第3期 郝国舜，等：一种扩展的动态描述逻辑语言及其Tableau算法 .227· 为了描述动态世界，人们也把动态逻辑中表示 形成的[4] 动作的机制引入到描述逻辑中来24)，形成了各种 但现有动态描述逻辑语言，都采用了不可分的 动态描述逻辑语言.但这些语言普遍采用不可分的 符号表示每个原子动作，不能对原子动作的各方面 符号来表示每个动作个体，无法通用地表示一类动 属性进行描述.而在很多计算系统中，动作属性是描 作，更无法表示不同动作实例之间可能存在的关系. 述动作的必要组成部分.一个操作名往往代表一类 因此，现有动态描述逻辑语言仍无法充分刻画计算 动作，需要通过各方面属性取值的不同来区别这类 系统的动态特征， 动作的具体动作实例比如：“借”作为一个操作名， 在已有动态描述逻辑基础上，借鉴程序语言的 代表了一类“借”动作（本文称为动作类）.假设在某 思想，在基本描述逻辑语言ALC(attribute language, 具体上下文中，它需要通过2个属性“主语”和“宾 C代表支持概念的否定)基础上，文中给出了一个扩 语”来描述，即此动作类可定义为：借（主语，宾语）· 展的动态描述逻辑语言(dynamic ALC with parame- 随着某些属性被赋予具体取值，这类动作逐渐派生 tc3 enabled).其中原子模态词不是用单个符号来表 或限制为越来越小范围的动作子类，比如，“主语” 示，而是由操作名和操作的参数集合形成，表示一类 被赋予具体的取值“张三”，就派生出动作子类：借 动作.随着参数被赋予具体的值，就形成了动作类和 (张三，宾语).当所有动作属性都被确定后，就得到 动作子类的层次关系.表示动作的模态词带有了参 只包含一个动作实例的动作子类，如以上宾语又被 数后，通过参数的不同取值来区别动作的行为是一 赋予值“描述逻辑手册（一本书）”后，就得到只包含 个重要的问题，本文通过对可达关系的限制表示动 1个动作实例的动作子类：借（张三，描述逻辑手 作的语义，可达的两世界不再是任意的，必须符合一 册).由此可见，类似描述逻辑中静态知识具有的层 定条件，此条件就与动作实例的各方面属性有关.模 次：概念、子概念和个体；对动作描述也需要有这样 态词中包含了参数后，对参数本身的语义解释也是 的层次关系：动作类、动作子类、动作实例.这种层次 需要解决的问题，本文都给出了符合现实意义的解 关系，不仅体现了动作类的共性，也体现了不同动作 释方法 实例间的差别，这对于充分描述动态系统并自动推 在给出的描述逻辑语言框架下，一个具体动作 理是非常重要的.现有动态逻辑用一个不可分的符 实例的语义由3个方面来决定：操作名、被作用的可 号来表示每个动作实例，就不能表示出这种动作类 能世界以及动作参数的取值，这与计算系统中动作 与动作实例间的层次关系.如在DLC中可用某个 的直观含义是一致的.另外，原子模态词由复合构造 原子动作模态词[心1]来表示某动作实，例如：借 子还可形成复合模态词；因此，本语言就可以对动作 (张三，描述逻辑手册)；采用另一个原子动作模态 进行2个维度的描述：动作类与动作实例、原子动作 词[2]来表示另一个原子动作实例如：借（张三， 与复合动作.文中还给出了此语言的Tableau算法， 人工智能).虽然2个模态词符号[1]、[a2]能够 从而证明了此语言是可计算的，可以应用于对具体 分别表示这2个原子动作，但表示不出来这2个原 计算系统的建模 子动作间的任何关系，即系统不知道[a1]、[2]所 代表的动作实例都属于“借”这个动作类，也都是发 1不可再分的符号难以表达动作的层 生在主语“张三”身上的.这2个动作间的重要关系 次关系 (都属于借这个动作类，都发生在张三身上，但有不 同的被作用对象)都丢失了， 描述逻辑是语义描述语言的逻辑基础，通过概 为了能够表达出上述动作的层次关系，本文借 念、概念的层次关系、个体之间的角色关系来刻画静 鉴程序理论的思想，扩充了原子模态词形式，使其不 态世界的知识.描述逻辑最初是为了描述静态世界 但包含操作名，还包含表示动作属性的参数集合.原 而设计的.为了提供描述动态世界的机制，人们把动 子动作类可由构造子形成复合动作类，原子动作类 态逻辑中表示动作的机制引人到描述逻辑中来，如 实例化生成具体原子动作，复合动作类也可实例化 典型的动态描述逻辑语言（命题动态逻辑(proposi-- 生成复合动作.其对应关系与程序理论是一致的：原 tional dynamic logic)与ALC的结合)就是通过把命 子语句构成复合语句，原子语句生成原子语句调用， 题动态逻辑2)引入到描述逻辑的基本语言ALC中 复合语句（即程序）生成复合语句调用（即进程），见
228. 智能系统学报 第4卷 图1所示.当然，这不是简单的把程序理论引入到逻 模态词动作的语义.下面就依次给出此扩展的动态 辑中，因为还必须要给出这些参数的语义如何定义， 描述逻辑语言DALCP的语法、语义，并讨论其相应 模态词的动作语义如何定义，以及参数如何影响了 算法与性质。 复合动作类 复合动作实例 程序以合诸) 进杜（世序运行实例 原子动作类 原子动作实例 原了语句 原了语句湖州 图1动作类与程序的对应关系 Fig.1 The correspondings between action classes and programs 2扩展的动态描述逻辑语言DALCP 4)如果中、p是断言，则中八p、中Vp、7中、m叫 也是断言，其中地称为模态断言. 2.1 DALCp的语法定义 2.2 DALCp的语义定义 定义1 DALCp的基本符号集合包括： 在定义DALCP的语义时，有2点与其他动态描 1)个体名：ao,a1,…,bo,b1,“ 述逻辑语言的不同：如何为参数赋予语义，以及参数 2)原子概念名：A,A,…,全概念T和空概念⊥； 如何影响模态词动作？为此，在传统动态描述逻辑 3）角色名：R,R,; 的模型M中，扩充2个元组J、更，其中：J表示对参 4)概念构造子：几，U,,3R,R 数的解释，中是关于原子模态词实例可达关系的限 5)操作名：α，操作参数集合：P; 制条件，此限制条件反映了模态词的动作.因此，语 6)操作参数的取值：1，，…； 言DALC,的模型具有从下形式： 7)原子模态词a4,ma2,…,复合模态词m。, M=〈W,{>m.Im。是原子模态词}，△，I,J,Φ). 2,统称模态词符号m1,m2,·; 模型中各个量的含义如下： 1)W是非空的可能世界集合. 8)复合模态词构造子：； 2)针对每个原子模态词实例，都有1个可达关 9)断言的逻辑连接符号：八，V以及括号[，] 系>m。·对于复合模态词实例，有下面公理给出其语 定义2 DALCp的模态词m定义如下： 义即对应的可达关系。 1)原子模态词：已知操作名α且此操作名代表 公理1复合模态词对断言的作用满足等式 的动作需要描述的属性集合为P,则[α(P)]是原子 模态词，可用符号m。表示； m1n2p=m2(1p）. 2)复合模态词：如果m1、m2是模态词（可以是 公理2复合模态词实例的可达关系满足：若当前 原子模态词，也可以是复合模态词)，则1°m2是复 可能世界为0，对任一复合模态词实例m=m,°m2,如 合模态词，可用符号。表示； 果01Dm02,02D03,则必然有：0Dm1m03 3)原子模态词和复合模态词都是模态词.当不 另外，计算机处理的动态系统一般都是确定性 刻意区分原子模态词或复合模态词时，一般可用模 的，对此，可规定可达关系具有下面的公理 态词符号m表示. 公理3可达世界的惟一存在性：对任意模态 由于篇幅所限，只讨论动作的连接这一复合动 词m和当前可能世界w∈W,存在且惟一存在可能 世界w'eW,与0具有可达关系：w>w'. 作构造子.对于其他如动作的并行、循环等构造子， 本文不详细讨论. 3)A为非空论域集合， 定义3 DALCP中的概念、角色、断言定义如下： 4)I是关于每个可达世界的解释函数I(和)= 1所有的原了概念，T、上都是概念： (△，R哈，…，C0,…,6,…） 2)所有的尔色名都足角色： 5)J是对参数的解释函数，把某个可能世界的 3）如果C、D是概念，R是角色，a、b是个体m 参数解释到系统的解释域上，J:P×W→A.对参数 为动作模态词，则CnD,CuD,C,3R.C,R.C都 的解释，基于以下约定： 概念，C(a,R(a.b).C三D都断言； a)参数被赋予的值可能是个体名、概念名，甚
第3期 郝国舜，等：一种扩展的动态描述逻辑语言及其Tableau算法 ·229 至知识库名，但总之都可看作是常量名； 态词动作的具体含义来给出，而不可能给出一个通 b)参数都被解释到被应用的可能世界中； 用的语义定义 c)对这些常量名的解释，等于“同名常量”在当 这里只举一个简单的例子来展示如何表示对可 前可能世界中的解释. 达关系的限制.比如，要表示以上借书动作的模态词 比如，假设当前可能世界为0，且01=P,对 a=[借（张三，描述逻辑手册）]的语义可以通过 [ax(P)]p中P的解释，就解释到当前可能世界0 Φ体现，其中Φ可以这样定义：若当前可能世界为 中，而不是作用后的可能世界中.用二元函数J表示 0∈W,V0'∈W,wDmw满足： 对参数的解释，这个函数可以规约为同名常量在当 若片图书馆的书（描述逻辑手册）， 前可能世界的解释I,即J(P,w)=P.根据P可能 则和仁张三手头的书（描述逻辑手册）. 为个体、概念，甚至数据库等形式，有下面的规约规 更通过给出关于模态词的2个可达世界和，w'之间 则： 满足的特定关系，来定义此模态词动作的语义.由此 J(C,w）=C4" 例容易看出，动作语义是与3个因素相关的：动作 J(a,w）=a", “借”改变了书所属的概念（从图书馆的书到张三手 J(R,0)=R', 头的书)；参数“张三”体现在了动作将被借个体改 J(C(a),w）=片J(a,w)∈J(C,o), 变为了属于概念“张三手头的书”；而参数“描述逻 J(R(a,b),w）== 辑手册”则是被动作的个体，其所属的概念在2个 (J(a,w),J(b,w))EJ(R,w), 可能世界间发生了改变. J(CED,w)=WFJ(C,W)EJ(D,w), 以上模型的定义，给出了所有原子成分的语义 J(7业，w)=w≠J(中，w）, 定义，包括个体、原子概念、角色和原子动作的语义 J(p∧中，w)=J(p,w)∧J(中，w), 通过下面的定义，把原子概念和公式的语义扩展到 J(pV中，w)=J(p,w)VJ(中，o). 所有语法成分上，给出语言DALCP的完整语义 因此，当前的可达世界0中，其实包含了2类知识， 定义4给定DALCp的模型M=〈W,{DmI。 一类是被动作作用的知识，一类是动作本身的知识， 为原子模态词}，△，I,J,Φ)和可能世界，则下面的 它们都属于0的解释域△“中. 满足关系均成立 6)中，对可达关系的限制 T4w=△"， 现有的动态逻辑或动态描述逻辑，采用Kripke 1"=中， 框架的语义解释方法定义模态词动作的语义，比如， (C)w=公\Cr 对模态词动作有如下定义：w=mg台Hw'∈W(w (CTD)"=C“nD, >w'→w=p).此定义直观解释为：模态断言mp (CUD)=C4"UD'", 为真，当且仅当，由”关于m可达的所有可能世界 (3RC)={xeAI3y∈， 和'都蕴含P为真这种方法来自于模态词必然口或 C.(x,y)∈R}, 可能◇的语义解释，实际并未真正表达出动态描述 (VRC)"={x∈△IHyA.((x,y)∈ 逻辑中模态词动作的含义，对于动态逻辑，其语义应 R→yeC")}, 强调模态词将当前世界中的断言作了怎样地变化， ECED今CwsD, 并使之变化为另一可能世界.因此，并非任意2个可 =C(a)-a"eC,", 能世界都具有可达关系.尤其对于提出的语言DAL R(a,b)(a!",B)ER'", C,其原子模态词的形式更加复杂，要对可能世界 0午7p台0≠p, 间的可达关系施加进一步的限制，才能表示出原子 w=pΛ中台w=p&F中， 模态词语义.本模型M中扩展的Φ就表示对可达关 w片pV中台w午p‖oFψ. 系的限制.这也是本语言语义定义与已有动态描述 2.3模态词规约规则 逻辑语言语义最大的不同.要注意的是，可达关系的 以上给出了模态词的语义定义.作为一个计算 限制中反映的是原子模态词实例的语义；但原子模 系统，更重要的是要能够根据语法，自动“计算”模 态词的语义，应该是根据被描述的具体领域中的模 态词的动作.这就需要给出模态词的语法规约规则
·230 智能系统学报 第4卷 同样，类似模态词动作的语义定义需要根据模态词 语言，Tableau算法可形式地检查ABox的协调性，因 特定的含义给出，模态词的规约规则也需要根据此 此，描述逻辑上的推理问题都可自动完成本文给出 特定含义给出.这里，只给出规约规则的一般形式 了扩展的描述逻辑语言DALCP以便描述资源的动态 2.3.1模态词规约规则 知识，而对此动态知识的推理也是智能性的重要基 用符号→表示单步规约规则.对于作用在某断 础本部分给出此语言的Tableau算法，借助此算法， 言p(p不包含模态词)上的原子模态词ma,文中有 网络环境的计算的智能性能够快速实现通过证明此 单步规约规则，以得到不包含模态词的结果断言： 算法的可终止性，还能够证明此算法是可计算的 。p地.其中，中也不包含模态词. 3.1语言DALCp的Tableau算法 根据复合模态词动作的语义定义，其规约规则可 传统的描述逻辑，为了证明ABox的协调性， 以通过下面给出的性质规约为原子模态词的动作， Tableau算法的基本思想就是构造ABos可能的模 性质1假设有复合模态词m。=m12,则对 型.通过消除连接词和量词，使得到的新的ABx 中，只包含原子断言形式.如果这些原子断言没有显 任意断言p,有(m1°m2)p→n1(m2p) 式的矛盾，如同时包含C(a)、7C(a),则形成的 这样，作用在某断言p上的模态词m,可以通过 ABox就是原ABox的一个模型.基本步骤如下： 多次应用以上单步规约规则，得到不包含模态词的 1)消除TBox:如果要检查的知识库包含TBox, 结果断言：mp→·中. 把概念的定义带人到ABox中，以消除TBox(即形成 2.3.2规约规则的性质 的ABox是针对空IBor的). 终止性、可靠性和完备性是模态词规约规则需 2)转化为否定正则形(negation normal form, 要具有的重要性质.本文只给出这些性质的定义，因 NNF):通过德摩根律(De Morgan's rules)和量词性 为对这些性质的检验，需要针对具体的系统，结合给 质，将被检查的概念（包括Assertion中的概念）中所 出的语义定义和规约规则来进行 有否定符号移动到原子概念名之前.这样的形式 1)终止性：规约规则的终止性意味着规则是否 称为否定正则形 充分，形式地定义如下. 3)构造Tableau树，并将此树完全展开：以被检 定义5对于任意给定的模态词m和任意给定的 查的ABor作为根节点，构造一个Tableau树.之后， 断言p或知识库KB,如果利用给定的规约规则，总能 根据给出的Tableau扩展规则扩展，直到再没有规 够将其规约为某个不包含模态词的结果断言中，即 则可用 p→业，或不包含模态词的结果知识库B',即： 4)检查完全扩展的Tableau树是否有不包含冲 mKB+·KB',则称给定的规约规则具有可终止性 突的叶节点.如有，则原知识库协调；否则不协调。 2)可靠性与完备性： 因此，Tableau算法也是一种构造性算法.针对 定义6如果规约规则满足下面的条件： 模态逻辑，也有相应的Tableau算法[)，其主要思想 ifmg→"业 就是引人对可能世界的分支.本文针对DALCP的 then V MVw Vw'.(0,o')∈Dm→(o=p→w=ψ)： Tableau算法，重点也在于如何处理模态词动作，其 则它们是可靠的. 他步骤与传统描述逻辑的完全一致，因此，在给出语 定义7如果规约规则满足下面的条件： 言DALCP的Tableau算法只给出针对模态词的展开 if yMYwVw'.(0,知')∈Dm→ 规则 (=p→w'=ψ) 针对模态词，有下面展开规则： then2p→'h. 1)→规则： 则它们是完备的. meg1,ma2,. 3语言DALCP的Tableau算法 .ma:1,2… 其中，有规约规则： 描述逻辑一大优势，就是其内部的形式推理机 map1w1, 制.借助概念构造子7、∩，其推理问题都可规约为 m.p2地2， ABx协调性问题).对于表示静态知识的描述逻辑
第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. 循此长度减少规律做证明。 因此，每个关于模态词的扩展规则使断言长度
,232. 智能系统学报 第4卷 减小，而断言长度是有限的，故有限步后，断言就可 模型.因此，对模态词的扩展规则保持了Tableau树 被展开成原子形式 的协调性.从左到右的性质由此得证 3.2.2可靠性 2)证明从右到左的性质 定义10(Tableau算法的可靠性)某个Tab- 从右到左的性质为：如果从Tableau树T扩展 lcau算法是可靠的，如果满足：若存在对此ABox协 后的树T协调，原树T必然也协调。对此性质的证 调性的Tableau证明，则此ABox必然协调. 明，采用类似上述的证明方法，可以很容易检查对每 要证明Tableau算法的可靠性，需要先证明下 个扩展规则都成立，故此不再详细证明. 面的性质. 综合对性质2个方向的证明，性质1成立： 性质2若Tableau树T是由Tableau树T经过 证明3(Tableau算法的可靠性证明)给定任意 以上扩展规则得来，且模态词规约规则与模态词语 ABox,存在协调性的Tableau算法，即以此ABox为 义定义是一致的，则T协调，当且仅当T协调. 根节点的Tableau树T,必然可完全展开为协调的 证明2这个性质包含从左到右和从右到左2 T.根据性质1，则T必然也是协调的，即原来的 个方面，分别证明之 ABox协调，可靠性得证 1)证明从左到右的性质. 4 结束语 从左到右的性质可陈述为：若某个Tableau树 T'是由Tableau树T扩展得来，T协调则T协调.证 类似表达静态知识的概念、子概念与个体间的 明思路为：协调的Tableau树T必然存在协调的分 树型关系，动作也存在类似的动作类、动作子类以及 支，假设此分支为B,那么可检验对此分支经过每个 动作实例的树型关系.通过把程序理论引人到描述 扩展规则，得到的T树是否仍然协调.如果每个步 逻辑中，给出了一个可对静态和动态2个层次知识 骤的扩展规则能保证Tableau树的协调性，则多步 进行树型描述的动态描述逻辑语言，并且通过定义 扩展也能包含其协调性.同样，传统的描述逻辑扩展 模态词语义形式地描述了2个层次的相互作用.本 规则不再证明，本文只证明关于模态词的展开规则 语言的自动推理算法是可靠的和可终止的，因此可 的性质 用于实际动态系统的描述与动作行为的推理， 一规则：规测风二在原叶节点下 本文给出的Tableau推理算法是属于动作行为 层面的，即如何通过模态词规约规则最终消除动作 添加新叶节点，此叶节点将原前缀σ代表的可能世 模态词得到结果断言.此推理算法可自动推理动作 界w扩展到了由前缀σ.。代表新的可能世界w'. 产生的结果，但并未对动作本身的层次结构进行推 既然原ABo协调，σ代表的可能世界w满足： 理.表示静态世界的描述逻辑中，对概念层次本身进 p1,片p2,….基于模态词规约规则 行推理可得到概念的可满足关系以及概念间的包含 m.p1Ψ1， 关系，从而可由显式知识推理出隐含的知识.类似 2， 地，具有树型层次的动作类本身也需要在推理动作 的结果前，讨论动作本身的可满足关系和动作间包 以及规约规则与语义定义的一致性，有： 含关系的自动推理问题，这对于讨论具体动态系统 0=p1,则01, 中的某动作是否有意义以及动作的分解都是非常重 0=p2,则=2， 要的，是需要进一步研究的内容， 参考文献： 因此，原叶节点的协调模型必然也是新的叶节点的 协调模型 [1]BAADER F,CALVANESE D,MCGUINNESS D,et al. c:1°2gp The description logic handbook:theory,implementation, →。规则：根据公理1，可知规则 :(2(m1p)） and applications[M].Cambrige,UK:Cambridge University 中，原协调ABx的模型必然也是新叶节点的协调 Phe38,2003
第3期 郝国舜，等：一种扩展的动态描述逻辑语言及其Tableau算法 .233. [2]EMERSON E A.Temporal and modal logic M].Van 作者简介： LEEUWEN J.Handbook of theoretical computer science, 郝国舜，男，1978年生，博士研究 Volume B:formal models and sematics.Amsterdam: 生，主要研究方向为服务计算、描述逻 Elsevier and MIT Press,1990:995-1072. 辑、数据汇聚等.发表学术论文多篇，作 [3]GABBAY D,GUENTHER F.Handbook of philosophical 为第一作者发表的E检索论文4篇. logic,Volume II:extensions of classical logic [M].Dor- drecht,The Netherlands:Kluwer Academic Publishers, 1984. 马世龙，男，1953年生，教授、博士 [4 WOLTER F,ZAKHARYASCHEV M.Modal description 生导师，国家自然科学基金委员会第 logics:modalizing roles[J].Fundamenta Informaticae, 十、十一届信息科学部专家评审组成 1999,39(4):411438. 员、国防科工委国防基础研究基金专家 [5]WOLTER F,ZAKHARYASCHEV M.Dynamic description 评审组成员、亚洲软件基础学会执行委 logics[J].Advances in Modal Logic,2000,2:449-463. 员会委员、中国人工智能学会常务理事，Frontiers of Computer [6]FITTING M,MENDELSOHN R L.First-order modal logic Sciencein China编委.主要研究方向为自动推理及其应用研 [M].Norwell,USA:Kluwer Academic Publishers,1999. 究、网络环境下的计算模型和逻辑研究、海量信息处理的计 [7]BAADER F,SATTLER U.Expressive number restrictions 算模型研究.承担过多项国家“973”和“863”项目，并获得 in description logics[J].Joural of Logic and Computation, 1998年度教育部科技进步三等奖.发表学术论文80余篇， 1999,9(3):319-350. 出版学术专著2部， [8]FRANCESCO M D,MAURIZIO L,DANIELE N,et al. 眭跃飞，男，1963年生，研究员.主要 The complexity of concept languages [J].Information and 的研究方向为形式本体论的研究，用信 Computation,1997,134(1):1-58. 息熵研究概念分类，以及用描述逻辑研 [9]NUTT W.Algorithms for constraints in deduction and 究概念间的推理等.改进了Guntsch和 knowledge representation[D].Saarbrucken,Germany:U- Gedig关于Wong和Ziark猜测的结果； niversity of Saarland,1993. 证明了粗关系数据库中信息熵关于粗关系数据库的加细的单 调性；提出了分层在线调页算法等.发表学术论文17篇， 2009 IEEE International Conference on Intelligent Computing and Intelligent Systems (ICIS 2009) 2009EEE智能计算与智能系统国际会议 2009 IEEE International Conference on Intelligent Computing and Intelligent Systems (ICIS 2009)will be held on Novem- ber 20-22,2009,in Shanghai,China.You are invited to submit papers in all areas of Intelligent Computing and Intelli- gent Systems,All accepted papers will be published in the IEEE categorized conference proceedings,which will be in- cluded in IEEE Xplore and indexed by EI Compendex and ISTP. Contact us The secretary of ICIS 2009 Ms.Huoyan Xu Tel:+86021-37773603 Website:http://www.icis09.cn E-mail:icis09@126.com
