| 基于配对方法的自动定理证明 |
| |
| 引用本文： | 陈玉泉,陆汝占,余皓. 基于配对方法的自动定理证明[J]. 软件学报, 1997, 8(4): 271-277 |
| |
| 作者姓名： | 陈玉泉 陆汝占 余皓 |
| |
| 作者单位： | 上海交通大学计算机科学与工程系,上海,200030;上海交通大学计算机科学与工程系,上海,200030;上海交通大学计算机科学与工程系,上海,200030 |
| |
| 基金项目： | 本文研究得到国家自然科学基金资助. |
| |
| 摘 要： | ＰｅｔｅｒＢ．Ａｎｄｒｅｗｓ提出了自动定理证明的配对方法的理论和算法．本文针对该算法的缺点，给出了一个无需回溯的实现算法，并得到一个高阶逻辑的自动定理证明系统.
|
| 关 键 词： | 自动定理证明 配对 归结 关联 高阶逻辑 |
| 修稿时间： | 1996-04-05 |
AUTOMATIC THEOREM PROVING BASED ON MATINGS |
| |
| CHEN Yuquan,LU Ruzhan and YU Hao. AUTOMATIC THEOREM PROVING BASED ON MATINGS[J]. Journal of Software, 1997, 8(4): 271-277 |
| |
| Authors: | CHEN Yuquan LU Ruzhan YU Hao |
| |
| Affiliation: | Department of Computer Science and Engineering Shanghai Jiaotong University Shanghai 200030 |
| |
| Abstract: | This paper first introduces the theory and algorithm of mating method in automatic theorem proving advanced by Peter B. Andrews, and then gives an implementation algorithm without backtracking, finally obtains a theorem proving system for higher order logic. |
| |
| Keywords: | Automatic theorem proving mating resolution connection higher order logic |
| 本文献已被 CNKI 维普 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
