首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   7篇
  完全免费   5篇
  自动化技术   12篇
  2016年   2篇
  2013年   1篇
  2011年   1篇
  2009年   3篇
  2008年   1篇
  2007年   1篇
  2006年   1篇
  1998年   1篇
  1992年   1篇
排序方式: 共有12条查询结果,搜索用时 187 毫秒
1.
动态描述逻辑的Tableau判定算法   总被引:6,自引:1,他引:5  
动态描述逻辑在描述逻辑的基础上引入了动态维,用于描述和推理动态领域的知识,但目前缺少有效的判定算法作为支撑.文中以描述逻辑ALCO的动态扩展为例,构建出动态描述逻辑D-ALCO.以D-ALCO的构建过程为基础,将ALCO的Tableau算法、命题动态逻辑的Tableau算法以及对可能模型途径的处理有机地结合起来,给出了D-ALCO的Tableau判定算法,证明了算法的可终止性、可靠性和完备性.应用该算法,可以在采用开世界假设的情况下对D-ALCO中公式的可满足性进行判定.对于D-ALCQO、D-ALCQIO等具有更强描述能力的动态描述逻辑,可以对该算法扩展后得到相应的Tableau判定算法.  相似文献
2.
基于可达关系的安全协议保密性分析   总被引:3,自引:0,他引:3  
借助形式化的方法或工具分析安全协议是非常必要而且行之有效的.进程演算具有强大的描述能力和严格的语义,能够精确刻画安全协议中各个参与者之间的交互行为.作者以进程演算为基础,嵌入消息推理系统以弥补进程演算固有的缺乏数据结构支持的特点,尝试地提出了一个基于可达关系的安全协议保密性分析模型.基于此模型,形式化地描述了安全协议的保密性,证明了一定限制条件下的可判定性.并且以TMN协议为例,给出了该模型的实例研究.  相似文献
3.
本文论述了尽管各种非调推理模式在形式表达方面,在语义解释方面都有不同的体现,但非单调推理在相当层次上具备如下三个特征:一是一般我们所理解的非单调性;二是知识增长的不确定性和认识的容错性;最后如何非要坚持正确性和完全性,便是非单调计算的困难性,一般是半不可判定的。  相似文献
4.
判定问题是逻辑研究中的重要问题.本文讨论了关于带有索引的认识逻辑ELI的基于语义tableau方法的判定过程,阐明了ELI的Mwff的可判定性.由于认识逻辑EL的公式与ELI的Mwff是对应的,因而,认识逻辑EL也是可判定的.  相似文献
5.
空间逻辑作为一个模态逻辑,能很好地描述分布式系统的行为和空间属性。其中,逻辑公式的有效性、可满足性及模型检测问题的可判定性已经得到广泛的研究。本文即是关于空间逻辑可判定性的一个综述,为此首先提出一个空间逻辑的定义框架,据此可以构造各种空间逻辑,并对它们的可判定性进行考察,从而指出影响空间逻辑的可判定性的关键因素。  相似文献
6.
周绪川  钟勇  蔡利平 《计算机工程》2011,37(11):187-189
针对多智能体系统(MAS)中执行决策的非确定性问题,研究结合时态/模态逻辑及机会发现理论,引入基于Kripke结构的复合逻辑 ,用于Agent的知识系统(全局知识、局部知识)及机会发现的形式化描述,为实现动态并发环境中MAS的系统协作行为建模及自动决策推理提供依据。给出 的结构及语义,证明了 的可判定性,且计算可在多项式级时间复杂度内实现。  相似文献
7.
描述了访问控制和逻辑的关系,并将访问控制授权判决问题归约成逻辑蕴涵问题;总结了基于逻辑的访问控制的基本逻辑问题,即逻辑基础、可判定性和安全性分析;分析了一些访问控制模型的基本逻辑问题,包括基于身份的访问控制模型、基于信任管理的访问控制模型和基于属性的访问控制模型;指出了结构化属性描述能力和安全性分析是基于逻辑的访问控制需要进一步研究的问题.  相似文献
8.
9.
开放逻辑是用于刻画知识的增长,更新及假说进化的一个引人注目的形式逻辑理论。文中描述了在开放逻辑中什么是典型的证明论问题,并形式地定义了开放证明的概念。关于开放逻辑中的判定性问题,得到的结论是:(1)一致的开放逻辑系统的开放证明问题是半可判定的(文中给出了一个判定算法);(2)不一致的开放逻辑系统的开放证明问题不是半可判定的。  相似文献
10.
林运国  李永明 《软件学报》2016,27(12):2994-3002
为了刻画开放量子系统的量子属性,扩展现有的量子马尔可夫链是有必要的.通过构建Exogenous量子算子逻辑,定义了Exogenous量子马尔可夫链.作为新型量子马尔可夫链,重点研究了4种可达性公式,给出可达性公式可满足性问题的求解,并分析了它们的可判定性问题.作为应用,实例说明广义量子Loop程序的终止问题可以归结为Exogenous量子马尔可夫链的最终可达性,进而通过检测量子公式可满足性来判定程序的终止问题.  相似文献
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号