WE COMPLETE ALGORITHM FOR AUTOMATED THEOREM PROVING
几何定理机器证明的WE完全方法

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.