%0 Journal Article %A NING Xinran %A XU Yang %A CAO Feng %A WU Guanfeng %T Clause Elimination Methods in First-Order Logic Lifted from Propositional Logic %D 2019 %R 10.3778/j.issn.1002-8331.1810-0305 %J Computer Engineering and Applications %P 18-25 %V 55 %N 5 %X 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. %U http://cea.ceaj.org/EN/10.3778/j.issn.1002-8331.1810-0305