命题逻辑提升到一阶逻辑上的子句消去方法

• 作者: 吴贯峰 宁欣然 徐扬 曹峰
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 一阶逻辑 蕴含模归结 子句消去方法 命题逻辑
• 年，卷（期）: 2019,（5）
• 所属期刊栏目: 热点与综述
• 页码范围: 18-25
• 页数: 8页
• 分类号: TP391
• 字数: 12551字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.1810-0305

摘要

在基于命题逻辑的可满足性问题(SAT)求解器和基于一阶逻辑的定理证明器上,子句集简化一直是必不可少的步骤,而其中子句消去方法在这些子句集简化方法中是非常重要的组成部分.将命题逻辑中的子句消去方法归结隐藏恒真消去方法(RHTE)和归结隐藏包含消去方法(RHSE)提升到一阶逻辑上,并且利用蕴含模归结原则(IMR)证明了这种提升方式在一阶逻辑上具有可靠性(Soundness),即依据这两种子句消去方法删除一阶逻辑公式集中的子句,并不会改变公式集的可满足性或者不可满足性.此外,将这两个方法与一阶逻辑子句消去方法锁子句消去方法(BCE)和归结包含消去方法(RSE)进行组合推广,发展得到一阶逻辑上新型子句消去方法(BC+RHS)E、(RS+RHT)E和(RHS+RHT)E,并且证明了这3种子句消去方法在一阶逻辑上的可靠性.最后,分析比较了这些子句消去方法的有效性,并且证明了这3种新型子句消去方法比组成它们的原始子句消去方法均具有更高的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	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