| 带量词的合一算法 |
| |
| 引用本文： | 李大法.带量词的合一算法[J].清华大学学报(自然科学版),1992(3). |
| |
| 作者姓名： | 李大法 |
| |
| 作者单位： | 应用数学系 |
| |
| 摘 要： | Ｒｏｂｉｎｓｏｎ于 １９６５年提出了归结原理，其主要工作是 Ｕｎｉｆｉｃａｔｉｏｎ算法。这个算法只能处理不带量词的子句公式，它不能用来发现定理的自然演绎证明。本文的算法能处理量词，它能用在基于自然演绎的定理证明系统上。文中给出合一定理的证明，基于此算法的自动自然演绎系统已实现，用它证明了Ａｎｄｒｅｗｓ；Ｂｌｅｄｓｏｅ和Ｐｅｌｌｏｔｉｅｒ挑战性问题。
|
| 关 键 词： | 自然演绎 一阶逻辑 归结 自动定理证明 合一算法 |
Unification algorithm with quantifiers |
| |
| Li DafaIntelligence Technology and System Laboratory.Unification algorithm with quantifiers[J].Journal of Tsinghua University(Science and Technology),1992(3). |
| |
| Authors: | Li DafaIntelligence Technology and System Laboratory |
| |
| Institution: | Li DafaIntelligence Technology and System LaboratoryDepartment of Applied Mathematics |
| |
| Abstract: | Robinson proposed a unification algorithm in 1965. The algorithm can only treat clause formulas without quantifiers, it can not be usedto find natural deduction proofs of theorems. Our algorithm can treatquantifiers, so it can be uesd in ATP system based on natural deduction.The unification theorem for the algorithm is proved. The automatic natural deduction proving system based on the algorithm has been implemented, the Andrews, Bledsoe and Pelletier Challenges were proved by thesystem. |
| |
| Keywords: | natural deduction the first-order logic resolution theoremproving unification algorithm |
| 本文献已被 CNKI 等数据库收录！ |
