关于归纳证明的探讨 |
| |
作者姓名: | 钟发荣 孙永强 |
| |
作者单位: | 浙江师范大学计算机系,上海交通大学计算机系 金华 321004,上海 200030 |
| |
摘 要: | 归纳定理证明是一种难度较大且较有前途的一种自动定理证明方法。较早的归纳定理证明器是Boyer一Moore于1979年提出的BM证明器,BM证明器采用的是传统的结构归纳法,对所证公式中的每个函数项都根据其所谓归纳模板提出相应的归纳方案,然后对这个归纳方案进行分析、比较和整理,得出整个
|
关 键 词: | 归纳证明 自动定理证明 算法 计算机 |
本文献已被 CNKI 维普 等数据库收录! |
|
点击此处可从《计算机科学》下载全文 |
|