计算机工程与应用2019，Vol.55Issue(5)：18-25,8.DOI:10.3778/j.issn.1002-8331.1810-0305
命题逻辑提升到一阶逻辑上的子句消去方法
Clause Elimination Methods in First-Order Logic Lifted from Propositional Logic
摘要
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.关键词
一阶逻辑/蕴含模归结/子句消去方法/命题逻辑Key words
first-order logic/ implication modulo resolution/ clause elimination method/ propositional logic分类
信息技术与安全科学引用本文复制引用
宁欣然,徐扬,曹峰,吴贯峰..命题逻辑提升到一阶逻辑上的子句消去方法[J].计算机工程与应用,2019,55(5):18-25,8.基金项目
国家自然科学基金(No.61573057) （No.61573057）
中央高校基本科研业务费项目(No.2010JBZ010). （No.2010JBZ010）
