首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   4篇
  国内免费   1篇
  完全免费   5篇
  自动化技术   10篇
  2011年   1篇
  2009年   1篇
  2005年   1篇
  2003年   1篇
  2002年   1篇
  1997年   3篇
  1996年   2篇
排序方式: 共有10条查询结果,搜索用时 31 毫秒
1
1.
提高一阶多值逻辑Tableau推理效率的布尔剪枝方法   总被引:8,自引:1,他引:7  
刘全  孙吉贵 《计算机学报》2003,26(9):1165-1170
含有量词的一阶多值Tableau方法具有统一的扩展规则,并由Zabel等人给出了可靠性和完备性的证明,但由于扩展后的分枝随着真值数目的增加而呈指数的增加,因而影响了机器推理执行的效率,该文提出了布尔剪枝方法,将带符号的公式与集合的上集/下集联系起来,使含量词的一阶多值逻辑公式的扩展规则大大简化,进一步,通过对布尔剪枝方法的分析,建立了一类特殊一阶多值逻辑正则公式的更为简洁的Tableau推理方法,该方法使得含量词的一阶多值逻辑Tableau推理类同于经典逻辑Tableau方法。  相似文献
2.
非经典逻辑的语义tableau方法   总被引:3,自引:0,他引:3       下载免费PDF全文
1.引言自动推理作为自动定理证明的扩展,在计算机科学,特别是人工智能领域中占有重要的地位。许多系统,都是以推理系统作为其核心部分,因此自动推理的研究,对人工智能的其它分枝将产生深远的影响,它所提出的推理方法也被应用于人工智能的各个领域。目前主要的推理方法有:公理系统、自然演绎系统、归结系统、语义tableau系统,不同的方法对于不同的逻辑系统各有优劣。归结系统和语义tableau系统都比较适合于自动推理,其中归结系统与子句或合取范式CNF密切相关,对经典逻辑非常有效,但对于模态逻辑等非经典逻辑存在困难。首  相似文献
3.
基于算子模糊逻辑的不确定程度计算   总被引:1,自引:0,他引:1       下载免费PDF全文
程晓春 《软件学报》1997,8(7):525-534
本文提出并比较了在信度语义下,计算算子模糊逻辑中公式(集)模糊程度的3种方法——归结法、广义归结法和TABLEAU方法.  相似文献
4.
本文简单介绍了基于Tableau方法的程序综合系统-DTPS.DTPS系统以定理证明为基础,为构造一个满足程序规约的程序,只需证明的确存在一个满足条件的对象。如果这个证明存在,那么从证明中可抽取出一个满足该程序规约的程序。  相似文献
5.
程晓春 《软件学报》1997,8(7):525-534
本文提出并比较了在信度语义下,计算算子模糊逻辑中公式(集)模糊程度的3种方法--归结法、广义归结法和TABLEAU方法。  相似文献
6.
程晓春  刘叙华 《软件学报》1996,7(11):698-705
标记逻辑是一种重要的次协调逻辑,和|≈是标记逻辑中的2种推理关系.二者都是次协调的,可以用统一的方法处理一致的知识与不一致的知识,是单调的,有基于归结的证明论,但不能保持经典逻辑中合理的推理,如三段论.|≈是非单调的,在前提一致时等价于经典逻辑的推理关系,但缺少有效的证明论.本文将给出推理关系和|≈基于Tableau演算的可靠而且完备的判定方法.  相似文献
7.
本文基于TABLEAU方法,给出了模糊逻辑中一些至今缺少有效证明论的推理关系的证明论,也给出了作者提出的模糊择优蕴涵的判定过程.据此说明了Yager所给出的推理规则对其所讨论的模糊推理关系是不完备的.分析了本文对前提和结论分别构造TABLEAU推理树的方法在研究推理关系的相关性等方面的直观语义和作为模糊Prolog的推理机所具有的优越性.  相似文献
8.
tableau方法是一种接近于逻辑系统表示的自动推理方法,由于其直观性和通用性,易于计算机实现,成为目前最普及的自动推理方法之一。在提高系统效率方面,主要在相关技术和策略、理论和方法等方面进行了分析,并展望了未来的研究方向。  相似文献
9.
在实时系统的形式验证中,为了直接验证带有明显时间约束的性质,选用了一种被广泛接受的(线性时间)实时时序逻辑——度量区时序逻辑来描述待验证的性质;提出了基于迁移的扩展时间B chi自动机;构建了度量区时序逻辑的基于迁移的扩展时间B chi自动机。这样扩展了已有实时系统模型检测工具的性质规范语言的表达能力,使其能直接处理和验证带有明显时间约束的性质。实现的工具表明,该算法有效且可行,并且显著地减少了结果自动机节点和迁移的数量,从而降低了结果自动机的大小,有利于进一步的模型检测过程。  相似文献
10.
刘万伟  王戟  王昭飞 《软件学报》2009,20(8):2015-2025
为使符号化模型检验技术适用于全部ω-正规性质,研究了ETL(extended temporal logic)的符号化模型检验方法.首先,扩展了LTL(linear temporal logic)的Tableau方法,给出了ETL的Tableau构造方法,进而给出了该方法基于BDD(binary decision diagram)的符号化实现.同时,在NuSMV的基础上实现了支持ETL符号化验证的模型检验工具ENuSMV.该工具允许用户自定义时序连接子,从而可以检验全部ω-正规性质.实验结果表明,ETL性质能够被高效地采用符号化技术加以检验.  相似文献
1
设为首页 | 免责声明 | 关于勤云 | 加入收藏

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