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

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