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

	一阶谓词演算定理机器胆的余式方法
	刘卓军2 ; 吴尽昭 1
刊名	计算机学报
	1996
卷号	19 期号:10 页码:728
ISSN号	0254-4164
英文摘要	将一阶谓词演算的定理证明转化为代数簇的计算, 从而获得代数化的Herbrand过程. 又通过一阶多项式间的求余运算, 给出了余式方法并证明了它的完备性. 证明了归结原理是余式方法的一种特例.
语种	英语
内容类型	期刊论文
源URL	[http://ir.amss.ac.cn/handle/2S8OKBNM/47694]
专题	系统科学研究所
作者单位	1.北京大学 2.中国科学院数学与系统科学研究院
推荐引用方式 GB/T 7714	刘卓军,吴尽昭. 一阶谓词演算定理机器胆的余式方法[J]. 计算机学报,1996,19(10):728.
APA	刘卓军,&吴尽昭.(1996).一阶谓词演算定理机器胆的余式方法.计算机学报,19(10),728.
MLA	刘卓军,et al."一阶谓词演算定理机器胆的余式方法".计算机学报 19.10(1996):728.