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

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

关键词: 一阶逻辑, 蕴含模归结, 子句消去方法, 命题逻辑