基本信息来源于合作网站,原文需代理用户跳转至来源网站获取       
摘要:
在基于命题逻辑的可满足性问题(SAT)求解器和基于一阶逻辑的定理证明器上,子句集简化一直是必不可少的步骤,而其中子句消去方法在这些子句集简化方法中是非常重要的组成部分.将命题逻辑中的子句消去方法归结隐藏恒真消去方法(RHTE)和归结隐藏包含消去方法(RHSE)提升到一阶逻辑上,并且利用蕴含模归结原则(IMR)证明了这种提升方式在一阶逻辑上具有可靠性(Soundness),即依据这两种子句消去方法删除一阶逻辑公式集中的子句,并不会改变公式集的可满足性或者不可满足性.此外,将这两个方法与一阶逻辑子句消去方法锁子句消去方法(BCE)和归结包含消去方法(RSE)进行组合推广,发展得到一阶逻辑上新型子句消去方法(BC+RHS)E、(RS+RHT)E和(RHS+RHT)E,并且证明了这3种子句消去方法在一阶逻辑上的可靠性.最后,分析比较了这些子句消去方法的有效性,并且证明了这3种新型子句消去方法比组成它们的原始子句消去方法均具有更高的有效性.
推荐文章
一阶逻辑中的扩展子句消去原则
集合蕴涵模归结
一阶逻辑
蕴涵模归结
子句消去方法
预处理方法
命题逻辑中代数学的影子
命题逻辑
代数学
数理逻辑
二义性
自然逻辑与不自然逻辑刍议--以命题逻辑为例
自然逻辑
不自然逻辑
公理方法
自然演绎方法
三值Luk命题逻辑系统中逻辑理论的拓扑刻画
真度
相似度
伪距离
逻辑度量空间
相容性
闭逻辑理论,闭集
内容分析
关键词云
关键词热度
相关文献总数  
(/次)
(/年)
文献信息
篇名 命题逻辑提升到一阶逻辑上的子句消去方法
来源期刊 计算机工程与应用 学科 工学
关键词 一阶逻辑 蕴含模归结 子句消去方法 命题逻辑
年,卷(期) 2019,(5) 所属期刊栏目 热点与综述
研究方向 页码范围 18-25
页数 8页 分类号 TP391
字数 12551字 语种 中文
DOI 10.3778/j.issn.1002-8331.1810-0305
五维指标
作者信息
序号 姓名 单位 发文数 被引次数 H指数 G指数
1 徐扬 西南交通大学系统可信性自动验证国家地方联合工程实验室 186 1462 15.0 32.0
2 宁欣然 西南交通大学系统可信性自动验证国家地方联合工程实验室 6 6 2.0 2.0
3 曹峰 西南交通大学系统可信性自动验证国家地方联合工程实验室 1 2 1.0 1.0
4 吴贯峰 西南交通大学系统可信性自动验证国家地方联合工程实验室 1 2 1.0 1.0
传播情况
(/次)
(/年)
引文网络
引文网络
二级参考文献  (0)
共引文献  (0)
参考文献  (8)
节点文献
引证文献  (2)
同被引文献  (8)
二级引证文献  (0)
2010(1)
  • 参考文献(1)
  • 二级参考文献(0)
2014(3)
  • 参考文献(3)
  • 二级参考文献(0)
2015(4)
  • 参考文献(4)
  • 二级参考文献(0)
2019(2)
  • 参考文献(0)
  • 二级参考文献(0)
  • 引证文献(2)
  • 二级引证文献(0)
2019(2)
  • 引证文献(2)
  • 二级引证文献(0)
研究主题发展历程
节点文献
一阶逻辑
蕴含模归结
子句消去方法
命题逻辑
研究起点
研究来源
研究分支
研究去脉
引文网络交叉学科
相关学者/机构
期刊影响力
计算机工程与应用
半月刊
1002-8331
11-2127/TP
大16开
北京619信箱26分箱
82-605
1964
chi
出版文献量(篇)
39068
总下载数(次)
102
相关基金
国家自然科学基金
英文译名:the National Natural Science Foundation of China
官方网址:http://www.nsfc.gov.cn/
项目类型:青年科学基金项目(面上项目)
学科类型:数理科学
  • 期刊分类
  • 期刊(年)
  • 期刊(期)
  • 期刊推荐
论文1v1指导