On first-order theorem proving using generalized odd-superpositions Ⅱ

摘要

It is shown that the proof system using odd-superpositions Ⅱ is not complete. The reason leading to this incompleteness is that the use of idempotency rule is neglected. By defining the superpositions of first-order polynomials and zero, the concept of odd-superpositions Ⅱ is extended, and a complete proof system using the extended odd-superpositions Ⅱ is developed. In addition, this proof system is an improvement on remainder method; its completeness demonstrates actually that the remainder method using semantic strategy is still complete.