-
题名命题逻辑提升到一阶逻辑上的子句消去方法
被引量：1
- 1
-
-
作者
宁欣然
徐扬
曹峰
吴贯峰
-
机构
西南交通大学系统可信性自动验证国家地方联合工程实验室
-
出处
《计算机工程与应用》
CSCD
北大核心
2019年第5期18-25,共8页
-
基金
国家自然科学基金(No.61673320)
中央高校基本科研业务费专项资金(No.2682018ZT10)
-
文摘
在基于命题逻辑的可满足性问题(SAT)求解器和基于一阶逻辑的定理证明器上,子句集简化一直是必不可少的步骤,而其中子句消去方法在这些子句集简化方法中是非常重要的组成部分。将命题逻辑中的子句消去方法归结隐藏恒真消去方法(RHTE)和归结隐藏包含消去方法(RHSE)提升到一阶逻辑上,并且利用蕴含模归结原则(IMR)证明了这种提升方式在一阶逻辑上具有可靠性(Soundness),即依据这两种子句消去方法删除一阶逻辑公式集中的子句,并不会改变公式集的可满足性或者不可满足性。此外,将这两个方法与一阶逻辑子句消去方法锁子句消去方法(BCE)和归结包含消去方法(RSE)进行组合推广,发展得到一阶逻辑上新型子句消去方法(BC+RHS)E、(RS+RHT)E和(RHS+RHT)E,并且证明了这3种子句消去方法在一阶逻辑上的可靠性。最后,分析比较了这些子句消去方法的有效性,并且证明了这3种新型子句消去方法比组成它们的原始子句消去方法均具有更高的有效性。
-
关键词
一阶逻辑
蕴含模归结
子句消去方法
命题逻辑
-
Keywords
first-order logic
implication modulo resolution
clause elimination method
propositional logic
-
分类号
TP391
[自动化与计算机技术—计算机应用技术]
-
