OM FIRST-ORDER THEOREM-PROVING USING GENERALIZED ODD-SUPERPOSITIONS-II

It is shown that the proof system using odd-superpositions II is not c omplete. 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 II is e xtended, and a complete proof system Lsing the extended odd-superposit ions II is developed. In addition, this proof system is an improvement on remainder method; its completeness demonstrates actually that the remainder method Lasing semantic strategy is still complete.