一类扩展的动态描述逻辑

作为描述逻辑的扩展,动态描述逻辑为语义Web服务的建模和推理提供了一种有效途径.在将语义Web服务建模为动作之后,动态描述逻辑从动作执行结果的角度提供了丰富的推理机制,但对于动作的执行过程却不能加以处理.借鉴Pratt关于命题动态逻辑的相关研究,一方面,对动态描述逻辑中动作的语义重新进行定义,将每个动作解释为由关于可能世界的序列组成的集合;另一方面,在动态描述逻辑中引入动作过程断言,用来对动作的执行过程加以刻画.在此基础上提出一类扩展的动态描述逻辑EDDL(X),其中的X表示从ALC(attributive language with complements)到SHOIN(D)等具有不同描述能力的描述逻辑.以X为描述逻辑ALCQO(attributive language with complements,qualified number restrictions and nominals)的情况为例,给出了EDDL(ALCQO)的表判定算法,并证明了算法的可终止性、可靠性和完备性.EDDL(X)可以从动作执行过程和动作执行结果两个方面对动作进行全面的刻画和推理,为语义Web服务的建模和推理提供了进一步的逻辑支持.     

基于动态时序描述逻辑的动作理论

动态时序描述逻辑(DLTLDL)是一类描述逻辑的动态时序扩展。提出一种基于DLTLALCIO的动态域建模方法,利用该方法可构造出刻画动态域知识的DLTLALCIO理论,并解决动作推理中的框架问题和分支问题。动作推理问题,如动作可执行性和投影问题等,可归结为关于DLTLALCIO理论的推理问题,并最终归结为DLTLALCIO的公式可满足性问题。DLTLALCIO公式可表达动作和时间约束,相对于其他基于描述逻辑的动作形式,基于DLTLALCIO的动作形式在需要执行复杂查询,尤其是含时间或动作的查询的应用场合具有更好的适用性。     

一种分布式动态描述逻辑

分析了目前描述逻辑(DL)的研究现状和存在的问题,特别是动态描述逻辑(DDL)作为语义Web逻辑基础所存在的问题.针对语义Web的特点和需求,对DDL进行了扩充,提出了一种新的描述逻辑,即分布式动态描述逻辑(D3L),给出了D3L的语法和语义,并研究了D3L的推理机制,提出了两种推理方法: 直接推理和转化推理.与动态描述逻辑DDL相比,该D3L可以为语义Web提供更为合理的逻辑基础,弥补了DDL作为语义Web逻辑基础的不足.     

CDDL:动态描述逻辑的不确定性扩展

本体(Ontology)是语义Web中共享知识的形式化建模工具,其逻辑基础是描述逻辑.动态描述逻辑(DDL)具有同时表示静态和动态知识的优势.本文针对语义Web需要处理不确定性动态知识的需求,利用云模型对DDL进行不确定性扩展,提出了一种能够有效实现不确定性静态和动态知识进行表示和推理的不确定性动态描述逻辑CDDL.与...     

一种模糊动态描述逻辑

分析了目前描述逻辑DL的研究现状和存在的问题,特别是动态描述逻辑DDL作为语义Web逻辑基础所存在的问题。针对语义Web需要处理模糊和不精确知识的特点和需求,对DDL进行了模糊化扩充,提出了一种新的描述逻辑,即模糊动态描述逻辑FDDL。给出了FDDL的语法和语义,研究了FDDL的推理机制。与动态描述逻辑DDL相比,该FDDL可以为语义Web提供更为合理的逻辑基础,弥补了DDL作为语义Web逻辑基础的不足。     

基于动态描述逻辑的语义Web服务推理

语义Web服务的提出是为了解决Web服务资源在语义Web中的自动发现、组合和执行等问题,基本思路是将本体承载的静态知识与对Web服务动态功能的描述有机地结合起来.动态描述逻辑是描述逻辑的一种动态扩展,支持面向语义Web的对动作的描述和推理.文中利用动态描述逻辑DDL(SHOIN(D))的描述和推理功能,提出对语义Web服务进行建模和推理的一种有效途径.从OWL-S中的Process Model出发,将语义Web服务建模为基于DDL(SHOIN(D))的动作理论,其中,对应于Process Model中的原子过程,可以对输入、输出、局部变量、前提条件、结果等多个方面进行建模;对应于Process Model中的复合过程,可以相应地对数据流以及顺序、选择、乱序、条件、迭代、循环等控制结构进行刻画.以建模后得到的动作理论为基础,应用动态描述逻辑的推理机制,可以分别对语义Web服务的可实现性、可执行性、投影、规划等问题进行推理.这些推理功能为语义Web服务的自动发现和自动组合提供了有效的支持.     

基于动态描述逻辑DDL的动作理论

基于一阶谓词逻辑或高阶逻辑的动作理论与采用命题语言的动作理论之间存在一个关于描述和推理能力的鸿沟;作为描述逻辑的动态扩展,动态描述逻辑DDL为基于描述逻辑的动作刻画和推理提供了一种途径.系统地研究了基于DDL的动作表示和推理问题.首先,在应用描述逻辑对静态领域知识进行刻画的基础上,引入带参数的原子动作定义式和带参数的复...     

带测试动作的动态时序逻辑扩展

作为一种动态知识表示形式,动态时序逻辑(DLTL)尤适用于正规程序验证,然而它不直接支持测试动作,这使得其应用受到一定限制。为支持测试动作,提出一个DLTL扩展DLTL+和一个判定DLTL+公式可满足性的tableau算法,并给出了算法的正确性以及其时间复杂度为2O(n)的证明。分析表明,DLTL+提供了一种直接的、有效的测试动作支持方式,该方式比已知的其他方式更具有实际应用价值。     

动态描述逻辑推理的并行计算技术

在设计用于处理大规模本体和数据的推理引擎时,推理引擎的可扩展性是一个需要研究的重要问题.动态描述逻辑要在真实环境中获得成功应用,需要在推理中采用并行计算技术.提出了两种方法将并行计算技术应用于动态描述逻辑推理.方法1是设计分布式动态描述逻辑框架.分布式动态描述逻辑由若干独立的动态描述逻辑所组成,这些动态描述逻辑两两之间通过桥规则联系起来.提出了基于Tableau的分布式推理算法,从而为分布式动态描述逻辑提供了全局推理能力,并且该算法可以将大的推理任务分解为若干子任务,而这些子任务可以被不同的推理主体并行处理.方法2是并行化动态描述逻辑的Tableau算法的不确定分支.不确定分支的并行计算使得推理任务可以在若干独立机器上同时执行.最后,介绍了推理引擎的原型实现并评估了其性能.实验结果表明提出的两种方法取得了明显的推理加速效果.     

描述逻辑中基于边界的模块提取方法

模块化是优化本体推理的一种有效的手段,提出了一种针对推理的模块提取方法,该方法通过分析符号解释域的边界和公理之间的关系计算出基于边界的模块。文中给出该基于边界的模块的理论基础,并证明了其模块的正确性。在评估实验中,通过与最优模块和符号模块进行比较,基于边界的模块和最优模块大小很接近,非常适合对推理进行优化。     

描述逻辑中基于边界模块的推理方法*

模块化是优化本体推理的一种有效手段,提出了一种针对推理的模块提取方法,该方法通过分析符号 解释域的边界与公理之间的关系计算出基于边界的模块。给出该基于边界的模块的理论基础,并证明了其模块 的正确性。评估实验表明,基于边界的模块和最优模块大小很接近,并使用边界模块进行推理后,推理性能显著 提高。     

A survey on temporal logics for specifying and verifying real-time systems

Over the last two decades, there has been an extensive study of logical formalisms on specifying and verifying real-time systems. Temporal logics have been an important research subject within this direction. Although numerous logics have been introduced for formal specification of real-time and complex systems, an up to date survey of these logics does not exist in the literature. In this paper we analyse various temporal formalisms introduced for specification, including propositional/first-order linear temporal logics, branching temporal logics, interval temporal logics, real-time temporal logics and probabilistic temporal logics. We give decidability, axiomatizability, expressiveness, model checking results for each logic analysed. We also provide a comparison of features of the temporal logics discussed.     

用描述逻辑进行语义Web服务组合

针对面向服务功能的语义Web服务组合问题,特别是经典的人工智能规划方法无法有效地处理Web服务执行过程中动态产生的新个体,以及基于服务匹配的方法则无法充分利用服务I/O参数类型之间大量的语义关联等关键问题,通过动态逻辑和描述逻辑之间的对比研究,采用描述逻辑公理来刻画Web服务的IOPR(inputs,outputs, preconditions and results),扩展了基于动态逻辑的人工智能规划方法,提出了把语义Web服务组合问题转化为描述逻辑推理问题的方法,克服了经典的人工智能规划方法中的困难和基于服务匹配的服务组合方法的缺点.     

Event calculus and temporal action logics compared

We compare the event calculus and temporal action logics (TAL), two formalisms for reasoning about action and change. We prove that, if the formalisms are restricted to integer time, inertial fluents, and relational fluents, and if TAL action type specifications are restricted to definite reassignment of a single fluent, then the formalisms are not equivalent. We argue that equivalence cannot be restored by using more general TAL action type specifications. We prove however that, if the formalisms are further restricted to single-step actions, then they are logically equivalent.     

改进的描述逻辑框架Rough-SHOIN

针对具有不完备、多粒度特点的不确定知识表示,设计了一个粗糙描述逻辑框架--Rough-SHOIN,利用粗糙相似关系作为概念描述的基础,定义概念的粗糙上近似和下近似,实现不完备概念表达,在概念解释中引入上下文,实现在不同粒度上准确定义概念-对象间关系。在此基础上,给出Rough-SHOIN粗糙概念的语法、语义及知识库,并在不增加计算复杂度的前提下,定义Rough-SHOIN的推理规则。通过实例说明该框架的有效性。