带量词的合一算法

Unification algorithm with quantifiers

Ｒｏｂｉｎｓｏｎ于 １９６５年提出了归结原理，其主要工作是 Ｕｎｉｆｉｃａｔｉｏｎ算法。这个算法只能处理不带量词的子句公式，它不能用来发现定理的自然演绎证明。本文的算法能处理量词，它能用在基于自然演绎的定理证明系统上。文中给出合一定理的证明，基于此算法的自动自然演绎系统已实现，用它证明了Ａｎｄｒｅｗｓ；Ｂｌｅｄｓｏｅ和Ｐｅｌｌｏｔｉｅｒ挑战性问题。

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.