摘要
本文将一阶谓词演算的定理证明转化为代数簇的计算，从而获得了代数化的Ｈｅｒｂｒａｎｄ过程．又通过一阶多项式间的求余运算，给出了余式方法并证明了它的完备性．同时，我们证明了归结原理是余式方法的一种特例．
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.
出处
《计算机学报》
EI
CSCD
北大核心
1996年第10期728-734,共7页
Chinese Journal of Computers
基金
博士后科学基金
攀登计划项目基金
关键词
定理证明
多项式
余式
机器证明
Theorem proving, first-order polynomials, first-order algebraic varieties, remainders
