几何代数在定理证明中的消元与化简算法  

ALGORITHMS OF ELIMINATION AND SIMPLIFICATION BASED ON GEOMETRIC ALGEBRA IN AUTOMATIC PROVING OF GEOMETRIC THEOREM

作　　者：曹源昊[1] 李洪波[1] 

机构地区：[1]中国科学院数学机械化中心,北京100190

出　　处：《系统科学与数学》2009年第9期1189-1199,共11页Journal of Systems Science and Mathematical Sciences

基　　金：国家自然科学基金NSFC(10871195;60821002/F02);国家重点基础性研究基金NKBRSF(2004CB318001)资助项目

摘　　要：在符号计算中,最困难的一个地方是中间计算过程的表达式快速膨胀.基于不变量代数的符号几何计算为解决这个困难提供了可能.比如,利用零几何代数证明欧氏几何定理时,就可以给出很短的证明,甚至是单项式证明.中间的证明过程里有很多地方涉及到消元,展开,化简等问题.从程序实现的角度出发,在充分利用零几何代数计算特点的基础上,给出用于机器证明的消元、化简算法.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.

关 键 词：共形几何代数 零括号代数 几何自动推理 算法 

分 类 号：O187[理学—数学]