| 摘要: |
| ＰｅｔｅｒＢ．Ａｎｄｒｅｗｓ提出了自动定理证明的配对方法的理论和算法．本文针对该算法的缺点，给出了一个无需回溯的实现算法，并得到一个高阶逻辑的自动定理证明系统. |
| 关键词: 自动定理证明 配对 归结 关联 高阶逻辑 |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到国家自然科学基金资助. |
|
| AUTOMATIC THEOREM PROVING BASED ON MATINGS |
|
CHEN Yuquan,LU Ruzhan,YU Hao
|
| 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. |
| Key words: Automatic theorem proving mating resolution connection higher order logic |
