| On first-order theorem proving using generalized odd-superpositions Ⅱ |
| |
| 引用本文： | 吴尽昭,刘卓军.On first-order theorem proving using generalized odd-superpositions Ⅱ[J].中国科学E辑(英文版),1996(6). |
| |
| 作者姓名： | 吴尽昭 刘卓军 |
| |
| 作者单位： | Department of Mathematics，Peking University，Beijing 100871，China，Institute of Systems Science，Chinese Academy of Sciences，Beijing 100080，China |
| |
| 基金项目： | Project supported by the Chinese Climbing Project Foundation and China Postdoctoral Science Foundation. |
| |
| 摘 要： | 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.
|
| 关 键 词： | theorem proving first-order polynomials odd-superpositions Ⅱ generalized odd-superpositions Ⅱ odd-factors. |
| 本文献已被 CNKI 等数据库收录！ |
