%0 Journal Article %T WE COMPLETE ALGORITHM FOR AUTOMATED THEOREM PROVING
几何定理机器证明的WE完全方法 %A ZHANG JING-ZHONG %A YANG LU %A HOU XIAO-RONG %A
张景中 %J 系统科学与数学 %D 1995 %I %X In this paper, we propose an algorithm, which need not do decomposition of an algebraic set into the union of its irreducible varieties, to overcome the so-called "reducibility difficulty" in automated theorem proving. Employing Wu's division and Euclid's algorithm, we call it WE algorithm. %K Ascending chain %K Wu's division %K Euclid's algorithm
机器证明,完全方法,辗转伪除法 %U http://www.alljournals.cn/get_abstract_url.aspx?pcid=6E709DC38FA1D09A4B578DD0906875B5B44D4D294832BB8E&cid=37F46C35E03B4B86&jid=0CD45CC5E994895A7F41A783D4235EC2&aid=FFBD2FBBC4A4F08E9C9A07F1EC9EF764&yid=BBCD5003575B2B5F&vid=23CCDDCD68FFCC2F&iid=38B194292C032A66&sid=1E41DF9426604740&eid=334E2BB8B9A55ABB&journal_id=1000-0577&journal_name=系统科学与数学&referenced_num=5&reference_num=0