共查询到18条相似文献,搜索用时 140 毫秒
1.
时态描述逻辑ALC-LTL的Tableau判定算法 总被引:2,自引:2,他引:0
时态描述逻辑ALC-LTL将描述逻辑ALC的描述能力与线性时态逻辑LTL的刻画能力结合起来,在具有较强描述能力的同时还使得可满足性问题保持在EXPTIME-完全这个级别。针对ALC-LTL缺少有效的判定算法的现状,将LTL的Tableau判定算法与描述逻辑ALC的推理机制有机地结合起来,给出了ALC-LTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性。该算法具有很好的可扩展性。当ALC-工`I'I、中的描述逻辑从ALC改变为任何一个具有可判定性特征的描述逻辑X时,只需要对算法进行简单修改,就可以得到相应的时态描述逻辑X-LTL的Tableau判定算法。 相似文献
2.
段跃兴 《计算机应用与软件》2010,27(10)
描述逻辑是一族知识表示的形式化语言,是一阶谓词逻辑的可判定子集,已成为语义Web的理论基础.描述逻辑中ALC是最小命题封闭的,是其它描述语言的基础,而可判定是描述逻辑的最重要的问题,在ALC中Tableau算法巧妙地解决了这一问题,掌握ALC中的Tableau算法是理解各种描述逻辑中可判定性的基础.对ALC中的Tableau算法进行详细阐述,并对其关键的几个性质: 可终止性、完备性和判定性给出了证明,为研究SHOIN(D)中的Tableau算法及性质奠定了基础. 相似文献
4.
时态描述逻辑是将描述逻辑与时态逻辑相结合后得到的逻辑系统,具有较强的描述能力;但是大部分的时态描述逻辑都是将时态算子同时引入到概念和公式中,使得公式可满足性问题的计算复杂度过高。将描述逻辑ALC与分支时态逻辑CTL相结合,提出新的分支时态描述逻辑ALC-CTL。该逻辑没有将时态算子用于概念的构造过程,而是将时态算子引入到公式的构造中;从分支时态逻辑的角度看,相当于将CTL中的原子命题提升为描述逻辑中的个体断言。最终得到的逻辑系统不仅具有较强的刻画能力,还使得公式可满足性问题的复杂度保持在EXPTIME-完全这个级别。通过将CTL的Tableau判定算法与描述逻辑ALC的推理机制有机结合,给出了ALC-CTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性。 相似文献
5.
为了判定描述逻辑SHIN的ABox一致性,提出了一种Tableau算法。给定TBox T、ABox A和角色层次H,该算法通过预处理将A转换成标准的ABox [A],按照特定的完整策略将一套Tableau规则应用于[A],直到将它扩展成完整的ABox [A]为止。A与T和H一致,当且仅当算法能产生一个完整且无冲突的ABox [A]。算法所采用的阻塞机制可以避免Tableau规则的无限次执行,该机制允许一个新个体被在其之前创建的任意新个体直接阻塞,而不仅仅局限于其祖先。通过对算法的可终止性、合理性和完备性进行证明,算法的正确性得以确认。 相似文献
6.
为判定描述逻辑SHIQ的ABox一致性,提出一种Tableau算法。给定TBox几ABoxA和角色层次H,通过预处理将A转换成标准的ABox A’,按照特定的完整策略将一套Tableau规则应用于A,从而不断地对A’进行扩展,直到将其扩展成完整的ABoxA”为止。A、T和H一致,当且仅当算法能产生一个完整且无冲突的ABox A”。该算法采用的阻塞机制能防止Tableau规则被无限次执行,避免多余的规则应用。通过证明Tableau规则的执行次数为有限次,确认算法的可终止性。通过证明由A”能构造一个同时满足A、T和H的解释,确认算法的合理性。通过证明Tableau规则的执行不会破坏A’与H的一致关系,确认算法的完备性。 相似文献
7.
8.
在设计用于处理大规模本体和数据的推理引擎时,推理引擎的可扩展性是一个需要研究的重要问题.动态描述逻辑要在真实环境中获得成功应用,需要在推理中采用并行计算技术.提出了两种方法将并行计算技术应用于动态描述逻辑推理.方法1是设计分布式动态描述逻辑框架.分布式动态描述逻辑由若干独立的动态描述逻辑所组成,这些动态描述逻辑两两之间通过桥规则联系起来.提出了基于Tableau的分布式推理算法,从而为分布式动态描述逻辑提供了全局推理能力,并且该算法可以将大的推理任务分解为若干子任务,而这些子任务可以被不同的推理主体并行处理.方法2是并行化动态描述逻辑的Tableau算法的不确定分支.不确定分支的并行计算使得推理任务可以在若干独立机器上同时执行.最后,介绍了推理引擎的原型实现并评估了其性能.实验结果表明提出的两种方法取得了明显的推理加速效果. 相似文献
9.
10.
为了判定SHIF的ABox一致性,提出了一种Tableau算法.该算法先通过预处理将ABox转换成标准形式,然后按照特定的完整策略将一套Tableau规则应用于ABox,直到将它扩展成完整的ABox为止.ABox与TBox一致,当且仅当算法能产生一个无冲突的完整的ABox.算法所采用的阻塞机制可以避免Tableau规则的无限次执行.为了提高算法的效率,该机制允许一个新个体被在其之前创建的任意新个体直接阻塞,而不仅仅局限于其祖先.通过对算法的可终止性、合理性和完备性进行证明,算法的正确性得以确认. 相似文献
11.
一类扩展的动态描述逻辑 总被引:4,自引:0,他引:4
作为描述逻辑的扩展,动态描述逻辑为语义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服务的建模和推理提供了进一步的逻辑支持. 相似文献
12.
13.
基于动态描述逻辑DDL的动作理论 总被引:1,自引:1,他引:0
基于一阶谓词逻辑或高阶逻辑的动作理论与采用命题语言的动作理论之间存在一个关于描述和推理能力的鸿沟;作为描述逻辑的动态扩展,动态描述逻辑DDL为基于描述逻辑的动作刻画和推理提供了一种途径.系统地研究了基于DDL的动作表示和推理问题.首先,在应用描述逻辑对静态领域知识进行刻画的基础上,引入带参数的原子动作定义式和带参数的复... 相似文献
14.
15.
Model Checking Markov Chains with Actions and State Labels 总被引:2,自引:0,他引:2
Baier C. Cloth L. Haverkort B.R. Kuntz M. Siegle M. 《IEEE transactions on pattern analysis and machine intelligence》2007,33(4):209-224
In the past, logics of several kinds have been proposed for reasoning about discrete-time or continuous-time Markov chains. Most of these logics rely on either state labels (atomic propositions) or on transition labels (actions). However, in several applications it is useful to reason about both state properties and action sequences. For this purpose, we introduce the logic as CSL which provides a powerful means to characterize execution paths of Markov chains with actions and state labels. asCSL can be regarded as an extension of the purely state-based logic CSL (continuous stochastic logic). In asCSL, path properties are characterized by regular expressions over actions and state formulas. Thus, the truth value of path formulas depends not only on the available actions in a given time interval, but also on the validity of certain state formulas in intermediate states. We compare the expressive power of CSL and asCSL and show that even the state-based fragment of asCSL is strictly more expressive than CSL if time intervals starting at zero are employed. Using an automaton-based technique, an asCSL formula and a Markov chain with actions and state labels are combined into a product Markov chain. For time intervals starting at zero, we establish a reduction of the model checking problem for asCSL to CSL model checking on this product Markov chain. The usefulness of our approach is illustrated with an elaborate model of a scalable cellular communication system, for which several properties are formalized by means of asCSL formulas and checked using the new procedure 相似文献
16.
17.
18.
基于动态描述逻辑的多主体协作模型 总被引:7,自引:2,他引:7
基于动态描述逻辑的主体模型和协作过程就是既考虑了智能主体的知识表示与推理问题,又紧密地结合主体的设计与编程问题,把表示与推理应用到主体的具体设计中.它充分利用了动态描述逻辑的统一的形式化框架,同时从静态的知识表示与推理和动态的运行与变化两个方面来刻画主体的心智状态和协作过程,探讨了主体信念、行为能力、目标和规划等心智要素的表示、推理与修改以及联合目标的形成、多目标的规划问题.多主体协作模型将理论和实践有机地结合起来,能够充分体现智能主体的本质特征与运行机制,为多主体系统的设计与编程奠定了很好的基础. 相似文献