%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