| 命题逻辑提升到一阶逻辑上的子句消去方法 |
| |
| 引用本文： | 宁欣然,徐扬,曹峰,吴贯峰.命题逻辑提升到一阶逻辑上的子句消去方法[J].计算机工程与应用,2019,55(5):18-25. |
| |
| 作者姓名： | 宁欣然 徐扬 曹峰 吴贯峰 |
| |
| 作者单位： | 西南交通大学 系统可信性自动验证国家地方联合工程实验室,成都,610031;西南交通大学 系统可信性自动验证国家地方联合工程实验室,成都,610031;西南交通大学 系统可信性自动验证国家地方联合工程实验室,成都,610031;西南交通大学 系统可信性自动验证国家地方联合工程实验室,成都,610031 |
| |
| 基金项目： | 国家自然科学基金;中央高校基本科研业务费专项资金 |
| |
| 摘 要： | 在基于命题逻辑的可满足性问题（SAT）求解器和基于一阶逻辑的定理证明器上，子句集简化一直是必不可少的步骤，而其中子句消去方法在这些子句集简化方法中是非常重要的组成部分。将命题逻辑中的子句消去方法归结隐藏恒真消去方法（RHTE）和归结隐藏包含消去方法（RHSE）提升到一阶逻辑上，并且利用蕴含模归结原则（IMR）证明了这种提升方式在一阶逻辑上具有可靠性（Soundness），即依据这两种子句消去方法删除一阶逻辑公式集中的子句，并不会改变公式集的可满足性或者不可满足性。此外，将这两个方法与一阶逻辑子句消去方法锁子句消去方法（BCE）和归结包含消去方法（RSE）进行组合推广，发展得到一阶逻辑上新型子句消去方法（BC+RHS）E、（RS+RHT）E和（RHS+RHT）E，并且证明了这3种子句消去方法在一阶逻辑上的可靠性。最后，分析比较了这些子句消去方法的有效性，并且证明了这3种新型子句消去方法比组成它们的原始子句消去方法均具有更高的有效性。
|
| 关 键 词： | 一阶逻辑 蕴含模归结 子句消去方法 命题逻辑 |
Clause Elimination Methods in First-Order Logic Lifted from Propositional Logic |
| |
| NING Xinran,XU Yang,CAO Feng,WU Guanfeng.Clause Elimination Methods in First-Order Logic Lifted from Propositional Logic[J].Computer Engineering and Applications,2019,55(5):18-25. |
| |
| Authors: | NING Xinran XU Yang CAO Feng WU Guanfeng |
| |
| Affiliation: | National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu 610031, China |
| |
| Abstract: | Simplifications of CNF formulas play a very important role on propositional SAT solvers and first-order theorem provers. And clause elimination methods are significant components of those simplification methods. In this paper, clause elimination methods in propositional logic Resolution Hidden Tautology Elimination（RHTE） and Resolution Hidden Subsumption Elimination（RHSE） are lifted to first-order logic and their soundness have been proved by using the principle implication modulo resolution, which means removing clauses in first-order CNF formulas according to the two clause elimination methods will not change the satisfiability or unsatisfiability of the original CNF formulas. Besides, three new generalized clause elimination methods are developed in this paper by combining the two clause elimination methods with other current clause elimination methods in first-order logic, separately called as（BC+RHS）E, （RS+RHT）E and（RHS+RHT）E. Finally, the effectiveness of clause elimination methods has been analyzed and compared. It shows that the new generalized three clause elimination methods have high effectiveness than those original clause elimination methods. |
| |
| Keywords: | first-order logic implication modulo resolution clause elimination method propositional logic |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与应用》浏览原始摘要信息 |
|
点击此处可从《计算机工程与应用》下载全文 |
|
