A Combined Method Based on Extension Rule and Resolution

Theorem proving based on the extension rule is a new reasoning method. It is, in a sense, potentially a complementary method to resolution based method. HRIER is a very fast extension rule algorithm with reduction rules and heuristic function. DR is a fast ordering-based restricted resolution method in proposition logic. In order to make best use of the respective characteristic of the extension rule method and resolution method, this paper proposes a combined algorithm CDE based on HRIER and DR. And then the soundness and completeness of it are proved. The experiment results show CDE is a fast SAT solver.