THE SUB-RESULTANT METHOD FOR AUTOMATED THEOREM PROVING
几何定理机器证明的结式矩阵法

In this paper, we present a method, with which ascending chains need not be factorized beforehand, to overcome the so-called "reducibility difficulty".Employing Wu's division and sub-resultant computations,we call it WR decomposition algorithm.