期刊文献+

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

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. 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.
出处 《Science China(Technological Sciences)》 SCIE EI CAS 1996年第6期608-619,共12页 中国科学(技术科学英文版)
基金 Project supported by the Chinese Climbing Project Foundation and China Postdoctoral Science Foundation.
关键词 theorem proving FIRST-ORDER polynomials odd-superpositions GENERALIZED odd-superpositions odd-factors. theorem proving,first-order polynomials,odd-superpositions Ⅱ,generalized odd-superpositions Ⅱ,odd-factors.
  • 相关文献

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部