| 一阶谓词演算定理机器证明的余式方法 | |
| 吴尽昭 ; 刘卓军 | |
| 2014-07-02 ; 2014-07-02 | |
| 关键词 | 定理证明 一阶多项式 一阶代数簇 余式 |
| 中文摘要 | 本文将一阶谓词演算的定理证明转化为代数簇的计算，从而获得了代数化的Ｈｅｒｂｒａｎｄ过程．又通过一阶多项式间的求余运算，给出了余式方法并证明了它的完备性．同时，我们证明了归结原理是余式方法的一种特例． |
| 语种 | 中文 |
| 出版者 | 计算机学报 ，1996年10期 |
| 其他责任者 | 北京大学数学系 ; 中国科学院系统科学研究所 |
| 内容类型 | 期刊论文 |
| 源URL | [http://ir.calis.edu.cn/hdl/530500/642]  |
| 专题 | 广西民族大学 |
| 推荐引用方式 GB/T 7714 | 吴尽昭,刘卓军. 一阶谓词演算定理机器证明的余式方法[J],2014, 2014. |
| APA | 吴尽昭,&刘卓军.(2014).一阶谓词演算定理机器证明的余式方法.. |
| MLA | 吴尽昭,et al."一阶谓词演算定理机器证明的余式方法".(2014). |
| 个性服务 |
| 查看访问统计 |
| 相关权益政策 |
| 暂无数据 |
| 收藏/分享 |
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论