A New Method for the Boolean Ring Based Theorem Proving

A new method for first-order theorem proving based on the Boolean ring approach is proposed. The method is an extension of Hsiangʹs N-Strategy in two aspects: (1) When the input polynomials are derived from clauses, our method is reduced to a more restricted (but still complete) version of N-Strategy: Only maximal atoms in an N-rule are considered for generating new inferences. (2) When the input polynomials are derived from non-clausal formulas, no new inference rules are needed in our method for ensuring the completeness. Unlike Kapur and Narendranʹs method which considers every pair of polynomials for superposition, our method restricts the pairs to those one of which consists of an odd number of monomials. The completeness proof of our method with the integration of reduction is also provided and is done by using the technique of semantic trees. The same technique is used to prove the completeness of N-strategy with reduction (using only N-rules and P-rules) for clausal theorem proving, thus it settles a longtime open problem.