Om first-order theorem proving using generalized odd-superpositions II

CSpace

	Om first-order theorem proving using generalized odd-superpositions II
	Wu, JZ; Liu, ZJ
	1996-12-01
发表期刊	SCIENCE IN CHINA SERIES E-TECHNOLOGICAL SCIENCES
ISSN	1006-9321
卷号	39 期号:6 页码:608-619
摘要	It is shown that the proof system using odd-superpositions II is not complete. The reason leading to this incompleteness is that the use of idempotency rule is neglected. By defining the superpositions of first-order polynomials and zero, the concept of odd-superpositions II is extended, and a complete proof system Lsing the extended odd-superpositions II is developed. In addition, this proof system is an improvement on remainder method; its completeness demonstrates actually that the remainder method Lasing semantic strategy is still complete.
关键词	theorem proving first-order polynomials odd-superpositions II generalized odd-superpositions II odd-factors
语种	英语
WOS研究方向	Engineering ; Materials Science
WOS类目	Engineering, Multidisciplinary ; Materials Science, Multidisciplinary
WOS记录号	WOS:A1996WB01200007
出版者	SCIENCE CHINA PRESS
引用统计
文献类型	期刊论文
条目标识符	http://ir.amss.ac.cn/handle/2S8OKBNM/28734
专题	中国科学院数学与系统科学研究院
通讯作者	Wu, JZ
作者单位	CHINESE ACAD SCI,INST SYST SCI,BEIJING 100080,PEOPLES R CHINA
推荐引用方式 GB/T 7714	Wu, JZ,Liu, ZJ. Om first-order theorem proving using generalized odd-superpositions II[J]. SCIENCE IN CHINA SERIES E-TECHNOLOGICAL SCIENCES,1996,39(6):608-619.
APA	Wu, JZ,&Liu, ZJ.(1996).Om first-order theorem proving using generalized odd-superpositions II.SCIENCE IN CHINA SERIES E-TECHNOLOGICAL SCIENCES,39(6),608-619.
MLA	Wu, JZ,et al."Om first-order theorem proving using generalized odd-superpositions II".SCIENCE IN CHINA SERIES E-TECHNOLOGICAL SCIENCES 39.6(1996):608-619.