一阶谓词演算定理机器证明的余式方法  

REMAINDER METHOD FOR THE MECHANICAL THEOREM PROVING IN FIRST-ORDER PREDICATE CALCULUS

作　　者：吴尽昭[1] 刘卓军[1] 

机构地区：[1]北京大学数学系,中国科学院系统科学研究所

出　　处：《计算机学报》1996年第10期728-734,共7页Chinese Journal of Computers

基　　金：博士后科学基金;攀登计划项目基金

摘　　要：本文将一阶谓词演算的定理证明转化为代数簇的计算，从而获得了代数化的Ｈｅｒｂｒａｎｄ过程．又通过一阶多项式间的求余运算，给出了余式方法并证明了它的完备性．同时，我们证明了归结原理是余式方法的一种特例．By converting the theorem proving in first-order predicate calculus to the computation of algebraic varieties, an algebraic version of Herbrand procedure is derived. Furthermore, this paper Present the remainder method based on the remainder computation on first-order polynomials and shows that this method is complete. In addition, it is proved that resolution principle is a special case of remainder method.

关 键 词：定理证明 多项式 余式 机器证明 

分 类 号：TP399[自动化与计算机技术—计算机应用技术]