εLQ系统循环定义术语集的可满足性推理

来源 :广西师范大学 | 被引量 : 0次 | 上传用户:zhangxinyao1121
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
描述逻辑是知识表示的一种形式,而且在知识表示中,我们一般会假设一个知识表示系统总能在一个合理的时间内回答用户的查询,所以研究描述逻辑的人所感兴趣的就是这个推理的过程,即决策的过程.不管它的答案是肯定的还是否定的,总之它这个过程都是要结束的.所以,研究一个包含决策推理的问题的描述逻辑的计算复杂度是很重要的.而它推理问题的确定度和复杂度依赖正在使用的描述逻辑的表达能力.描述逻辑的表达能力制约着其推理问题的复杂度.表达能力很强的描述逻辑系统,它推理问题可能会变得很复杂.所以研究DL的表达能力与其推理复杂度是非常有必要的.循环定义可以增强描述逻辑的表达能力,而且在许多实际运用中都是不可避免的.除此之外,循环定义还能够为用户建立描述逻辑知识库,并使所表示的知识或公理符合人们的直觉,如果没有循环定义,用非循环定义来描述,这样就会使得知识库变得非常复杂,用户也会很难理解.所以,不管是从理论上,还是从实际运用上,研究描述逻辑循环定义都是很有价值的.  循环术语一直都是描述逻辑的研究难点,其基本的问题就是语义和推理问题没有得到合理的解决.本文就描述逻辑循环术语集的研究现状和存在的问题进行分析,将Badder的研究工作扩展到新的方向.针对更具有表达能力的描述逻辑系统,研究了循环术语集的语义及推理机制,蒋运承等人在描述逻辑εL的基础上添加了数量约束构造算子N提出了DL系统εLN,给出了εLN的语义(包括最大不动点语义、最小不动点语义和描述语义).并且根据Baader研究出的描述图之间的模拟关系的条件给出了不动点语义下εLN循环术语集的可满足性和包含关系推理算法,并证明了推理算法是多项式时间复杂的.  由εLN系统引出的思考,针对εL系统,增加在一定范围内的角色后继的数量约束构造算子Q,提出了描述逻辑系统εLQ,εLN与εLQ的区别就在于前者仅是后继的数量限制,后者是规定在一定范围内的后继的数量限制.根据εLQ的需要重新的定义了描述图(包括语法描述图和语义描述图).本文主要是在描述语义下讨论εLQ的可满足性.  从前人的工作中发现Badder的结论中的模拟条件G→T~GJ太抽象,太苛刻了,本文想舍去.试图从这一模拟的条件中寻找更为简单的方法,来研究这两图之间的关系即路径图之间的匹配关系.用路径匹配的方法判断其可满足性,从而将抽象的结论化为具体的,便于人理解的结论.  论文的主要工作:  (1)介绍描述逻辑的基本内容及其研究价值,循环定义及其术语集的研究现状,给出循环定义,特别是εLQ系统的语义及语法.根据εLQ系统的语义及语法重新画出相对应的语义描述图及语法描述图.  (2)研究εLQ系统的语义描述图及语法描述图,并利用Badder的模拟的条件来研究它们之间的关系.通过这一结论来验证我们引进的新的方法,路径匹配.  (3)给出路径匹配的定义,通过对个案的研究发现若两图匹配则语义描述图上的每一个节点都是被定义概念上的解.这样做的目的是让人站在另一角度去看待解即可满足性这一个定义,能更直观容易地理解可满足性这一个概念.只要一看到被定义概念的语义路径图,就可以马上判断它是否有非平凡解,解是什么.
其他文献
本文讨论有外力存在时可压缩粘性气体一维等熵等温模型方程组初边值问题的解的整体存在性和渐近性.即:当f≠0,x∈[0,1]时,方程组vt-ux=0,ut+(av-1)x=μ(ux/v)x+f(∫x0vdy,t)在初值
全光纤网络可定义为弧对称的有向图G(即α是G的一条弧当且仅当它的反向α-1也是G的一条弧)。设Rf(G)是G的一个f-容错路由集(f-fault tolerant routing)。Rf(G)中通过弧α的有向路的
我们知道w一无穷李代数W,W,由于在共形场论、量子场论等物理方面的广泛应用变得非常重要.广义W-无穷型(广义Weyl-型)李代数,由于它是无限维李代数,所以研究它的表示变得困难
现今电子结构计算的大规模化和结构新颖化,使得相关求解算法和计算软件得到快速发展。通过追踪分析BigDFT开源软件框架在研发过程中的相关算法创新和改进,本文基于多贝西密度泛函算法的不同标度法与多贝西约束性密度泛函理论的片段法进行研究,并结合高性能集群平台对电子结构计算模拟中出现的一些计算瓶颈和应用新方向进行计算分析。首先,基于多贝西小波密度泛函的立方标度、线性标度算法可以计算周期性和表面边界条件系统
学位