ALGORITHMS OF ELIMINATION AND SIMPLIFICATION BASED ON GEOMETRIC ALGEBRA IN AUTOMATIC PROVING OF GEOMETRIC THEOREM
几何代数在定理证明中的消元与化简算法

In symbolic computing, a major bottleneck is middle expression swell. Symbolic geometric computing based on invariant algebra can alleviate this difficulty. For example, the size of proofs of Euclidean geometric theorems can be reduced significantly based on null bracket algebra. In this paper, we consider algorithms of elimination, duality and ungrading in null bracket algebra from the viewpoint of program implementation.