论文部分内容阅读
描述逻辑（DLS)是一类知识表示的形式系统，其以结构化、形式化的方法定义应用领域的概念及刻画领域内的信息.描述逻辑具有强大的表达能力、有效推理等优点，它的核心是推理服务.一直以来描述逻辑受到人们的关注，描述逻辑在信息系统软件工程以及自然语言处理等领域得到了广泛的应用.特别是在第三代Web-语义网中扮演者关键角色，并成为W3C推荐Web本体语言OWL的逻辑基础. Nebel率先深入研究描述逻辑循环定义，提出循环定义的3种语义.接着F.Baader建立语法描述图GT和语义描述图GJ,使用描述图及图之间的模拟关系给出描述逻辑系统εL在循环定义下3中语义的被定义概念的可满足性推理和包含关系推理算法，并证明推理算法是多项式时间复杂的. 随着研究工作的深入，人们不满足于只带交算子和全称算子的描述逻辑系统FL0和只带交算子和存在算子的描述逻辑系统εL的表达力，许多人们在已有研究基础上通过增加构造子等方式继续研究.在此基础上，本文初步探讨增加角色的逆算子，角色的合成算子的描述逻辑系统IS-εL循环定义术语集的可满足性推理.本文并不针对F.Baader中循环定义的3种语义的某一种语义讨论，即不设定特定语义环境讨论可满足性.因为不管是在哪种语义下的可满足性，只要被定义概念是是有解的，那么其可满足.以Baader的结论1为起点，在最大不动点语义下，一个待定义的概念A∈Ndef是否可满足（在给定的基解释（△，J)中）要求的条件:存在一个语法描述图GT到语义描述图GJ的一个模拟:GT(≒)GJ该结论较一般化，具有概括性，也可以理解为要求的条件苛刻.本文认为该结论是一个抽象的一般化的结论，所以尝试从细节方面探讨，针对5个具体的循环定义依据其语法图和语义图采用路径匹配的方法判断其可满足性，继而抽象得出一般化的结论.也就是该5个循环定义有解的必要条件是:语义路径存在循环.5个循环定义有解的充要条件是:存在尾部循环的语义路径图使得语法路径图与之匹配，并且尾部循环的语义路径图上的结点就是被定义概念的解.使用路径图之间的匹配关系给出该5种被定义概念在IS-εL循环术语集的可满足性推理算法，并证明了推理算法是多项式时间复杂的.这样如果存在特定的语义路径图，则可以快速判断该路径上的结点是否是被定义概念的解.这样的结论是具有意义的.前人判断某元素是否是解的方法一般有:把某元素放到被定义式中验证看其是否满足左右的定义式或者根据在最大不动点语义下，根据Baader的结论1的方法寻找是否存在一个GT到GJ的一个模拟.不管怎样，这两种方法的共同特点在于:每个可能是解的元素都要一一验证.这对于计算机判断中是不够快速有效的.关于本文中判断是解结论中是根据特定的语义路径图的形状来判定的，并且得到的往往是一群相关元素是否是解的问题.如果把特定形状的语义路径图存储在计算机中再匹配，毫无疑问这样的匹配是快速有效率的，不需一一验证，可以节省更多时间和空间. 本文主要工作如下: 第二章，介绍了描述逻辑系统IS-εL的语法及语义等预备知识. 第三章，介绍描述图. 第四章，引入路径匹配的方法判断循环定义的可满足性. 本文的主要研究成果总结如下: 命题10N≡(3)r.N.其中α1∈GT,α2∈GJ. 若α2是一个由某x开始的复合路径，它的每一条边都是r.而且，每一单路径都以循环为尾部.令S={x|x是α2的结点元素}，N=S(C)△J,则以下3个结论成立: 1.α1与α2匹配; 2.S={x|x是α2的结点元素}.则N=S(C)△J是N≡(3)r.N的解; 3.结论1与结论2等价. 命题14 N=(3)r1.N(∏)(3)r2.N. α2∈GJ，若α2是由某x开始的复合路径，该路径上的每个结点分别存在r1，r2的边.而且，每一单路径都以循环为尾部.令S={x;x是α2的结点元素}，N=S(C)△J,则以下3个结论成立: 1.α1与α2匹配; 2.S={x|x是α2的结点元素}.则N=S(C)△J是N≡(3)r1.N(∏)(3)r2.N的解; 3.结论1与结论3等价. 命题16 N≡(3)r1.N1，N1≡(3)r2.N. α2∈GJ,α2是一个由某元素x开始的复合路径，它是以r1，r2（以r1或者r2开始）交替为边的多个起点的路径，而且，每一单路径都以循环为尾部.令S1={x|(3)y，(3)z，(x,y)∈r1∧(y，z)∈r2，x是α2的结点元素}，S2={x|(3)y，(3)z，(x，y)∈r2∧(y，z）∈r2，x是α2的结点元素}，S=S1∪S2={x|x是α2的结点元素}，N=S1(C)△J, N=S2(C)△J,则以下3个结论成立: 1.α1与α2匹配; 2.N=S1(C)△J，N1=S2(C)△J分别是N≡(3)r1.N1，N1≡(3)r1.N的解; 3.结论1与结论2等价. 命题19给定描述逻辑IS-εL的TBoxT是N≡(3)r.N，J1=（△J1，·J1），J2=（△J2，·J2）是两个不同的基解释.语法图GT=(Ndef, ET, LT)，语义图为G1J=（△J1，E1，L1），G2J=（△J2，E2，L2）.对于α∈GT,单路径β1∈G1J,单路径β2∈G2J,如果α与β1匹配，β1与β2匹配，那么α与β2匹配.