基于时态数据库的极小子结构逻辑系统

逻辑是知识表达的重要方法,但由于时序性知识与时间属性知识交叉应用的复杂性,其对时态数据库支撑一直不尽如人意.目前时态数据运算体系不完备,时态关系演算缺乏系统和有力的逻辑与代数理论支持.为此,文中从子结构逻辑出发,针对时态数据库及其信息处理中关键的知识推理、时态操作与函数依赖等内容,构建了一个极小的(最小的)子结构逻辑系统TDLrmin,其恰好等价于传统的数据库函数依赖Armstrong规则.TDLmin系统能在逻辑语义模型中对时序性、时间属性进行表达,而在句法逻辑系统将时间剥离,从而既表达了时态知识,对时态操作进行处理,又降低了逻辑系统的复杂度,使得逻辑系统的时间复杂度为P-time (O(n2)).而该逻辑系统还可与传统的Allen方法进行对接,使得相关时态查询所需的时间代价为传统非时态查询的时间加上一个复杂度仅为O(n)的线性时间,从而使得系统具有更强的普适性和应用前景.     

面向交互的主体能力描述和推理方法研究

主体间的交互对主体能力的影响是主体能力描述和推理需要考虑的一个重要因素．给出了一个面向交互的主体能力描述和推理框架．该框架将描述逻辑中的知识表示结构和任务逻辑中的任务语义结合起来，可以显式地描述主体之间的交互关系对主体能力的影响并可提供可判定的推理服务．建立了一个用于任务可完成性判定的逻辑系统DTL，并证明了它是可靠、完备和可判定的．     

分支时态描述逻辑ALC-CTL及其可满足性判定

时态描述逻辑是将描述逻辑与时态逻辑相结合后得到的逻辑系统,具有较强的描述能力;但是大部分的时态描述逻辑都是将时态算子同时引入到概念和公式中,使得公式可满足性问题的计算复杂度过高。将描述逻辑ALC与分支时态逻辑CTL相结合,提出新的分支时态描述逻辑ALC-CTL。该逻辑没有将时态算子用于概念的构造过程,而是将时态算子引入到公式的构造中;从分支时态逻辑的角度看,相当于将CTL中的原子命题提升为描述逻辑中的个体断言。最终得到的逻辑系统不仅具有较强的刻画能力,还使得公式可满足性问题的复杂度保持在EXPTIME-完全这个级别。通过将CTL的Tableau判定算法与描述逻辑ALC的推理机制有机结合,给出了ALC-CTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性。     

一种用于指针程序安全性证明的指针逻辑

在高可信软件的各种性质中,安全性是被关注的重点,其中软件满足安全策略的证明方法是研究的热点之一.文中根据作者所设想的安全程序的设计和证明框架,为类C语言的一个子集设计了一个指针逻辑系统.该逻辑系统是Hoare逻辑系统的一种扩展,它用推理规则来表达每一种语句引起指针信息的变化情况.它可用来对指针程序进行精确的指针分析,所获得的信息用来证明指针程序是否满足定型规则的附加条件,以支持程序的安全性验证.该逻辑系统也可用来证明指针程序的其它性质.     

中介逻辑ML的语法完全性

中介逻辑ML(MediumLogic)是近年提出的一种非经典逻辑。在ML的系统特征理论中已证明ML具有语义完全(完备)性。本文研究了ML的语法完全性,证明了如下结果:(1)ML中的中介命题逻辑系统MP及其扩张MP*是语法完全的,中介谓词逻辑系统MF与其扩张MF*,以及含有等词的中介谓词逻辑系统ME不是语法完全的。(2)一般地,如果一个协调的逻辑形式系统不是语法完全的,则它的任何协调的扩张系统也不是语法完全的。     

描述逻辑(FL0)的包含推理及其保守扩充

本体作为知识库表示知识已经成为计算机理论与应用的研究热点.在描述逻辑中,将本体看作一个逻辑理论,一个本体被形式化为给定的描述逻辑系统的一个Tbox.本体是动态的实体,为了适应新领域的发展,需要对原始本体进行扩充.但是扩充后的本体与原始本体是否保持逻辑一致性是目前研究者们所关注的焦点.在Lutz等人研究的基础上探究(FL0)的保守扩充问题.首先构建了(FL0)的典范模型,将包含推理问题转换为典范模型的模拟问题;其次由典范模型之间的最大模拟是多项式时间复杂的,证明了(FL0)的包含推理是多项式时间复杂的;最后给出描述逻辑(FL0)的保守扩充及其判定算法,证明了(FL0)的保守扩充的判定算法是指数时间复杂的.     

基于最大不动点模型的描述逻辑系统FLε的有穷基

研究了描述逻辑的有穷基问题,分析了有穷基在描述逻辑中的重要意义及其研究现状,并研究了形式概念分析中的属性蕴舍和Duguenne-Guigues基问题.利用形式概念分析中Duguenne-Guigues基存在的证明结果,在F.Baader工作基础上设置了描述逻辑的描述背景,重新定义了描述背景下的属性蕴含,证明了带循环术语的描述逻辑系统FLε存在最大不动点语义(greatest fixed-points,gfp)模型,给出了带循环术语的描述逻辑系统FLε在最大不动点模型下的有穷基的存在性定理,并证明有穷基的可靠性和完备性.描述逻辑有穷基可以帮助知识工程师构建一个更适用于推理的描述逻辑知识库.     

一种基于符号变换的描述逻辑ALC超协调推理算法

语义万维网作为一个开放、不断更新而且相互协作的环境,经常会包含一些不协调的或不精确的信息。众所周知,描述逻辑是语义万维网重要的逻辑基础,然而描述逻辑缺乏处理不协调或不完全信息的能力。近来一些超协调方案通过限制或阻止使用一些推理规则来避免推理的平凡化,从而容忍本体中出现的不协调。因为这些方法限制了描述逻辑系统的推理能力,所以推理能力弱于经典的描述逻辑推理能力,即使在处理协调的本体时。提出一种基于符号变换的具有强推理能力的超协调推理算法。证明了该算法是可判定的,而且在处理协调的本体时该推理系统与经典逻辑系统具有相等的推理能力。     

描述逻辑系统vL循环术语集的可满足性及推理机制

文中分析了描述逻辑循环术语集的研究现状和存在的问题,将近年来Baader F和Nebel B等人的工作扩展到新的方向.首先定义了描述逻辑的子系统vL,重新定义描述图G_T和G_J,使用互模拟的方法,给出了描述逻辑系统vL循环TBox非平凡的模型存在的、基于描述图的一个语法条件.证明:vL的包含推理算法是多项式时间复杂的.     

描述任务逻辑及其应用

针对任务逻辑存在的两个缺点：（1）不可判定，无法保证推理过程都能在有限的时间内结束；（2）任务的定义局限于抽象的、逻辑的定义。无法描述任务的具体属性和任务之间的关系，将描述性结构引入任务逻辑，构造了一个可描述具体属性的、可判定的任务逻辑系统——描述任务逻辑．将所构造的逻辑系统应用于具有组织的多主体系统行为建模，建立了基于描述任务逻辑的多主体组织模型和建模框架，并且表明应用描述任务逻辑构造应用系统具有表达能力强、结构紧凑的特点．