中文摘要：

在几何定理机器证明中, 使用几何不变量可以简化代数表示并导致代数处理的简化, 从而提高机器证明的效率和效果. 几何代数是最重要的一类由几何不变量组成的代数系统. 在代数处理中, 一个突出的困难是分解出真正表示几何原问题的代数成分, 称为几何分解. 在某种意义上, 机器证明是几何分解的特例, 后者的重要性超出机器证明本身. 本项目的主要内容是研究基于几何代数符号计算的几何分解. 在理论方面, 研究高维Clifford括号代数, 利用结式研究基于重写规则的代数分解. 在应用方面, 利用几何分解研究几何定理机器证明, 机器人的运动学和反运动学问题, 和基于不变量的景物欧氏重建. Clifford括号代数和几何分解是目前几何定理机器证明领域最前沿的内容之一, 对机器证明的理论和高科技应用有重大意义.

结论摘要：

笛卡尔坐标的引入，使得几何学从以定性刻画为主过渡到以定量计算为主，是人类思想史上划时代的事情。但是，坐标是一种参照物，本身没有几何意义，在应用中遇到代数结果的几何解释困难、代数计算的中间表达式膨胀两种主要障碍。微积分的发明人之一莱布尼兹有一个著名的梦想，希望能有一种几何计算可以直接处理几何体，而不是笛卡尔引入的一串数字。在十九世纪发展出来的、又在1970年代复兴的经典不变量理论，依然遇到同样的困难。只有高级不变量的引入和高级不变量理论的建立，才可能根本克服这些困难。 经过七年的努力，在2007年我们终于建立了经典几何的高级不变量理论体系。在经典几何的自动推理中，高级不变量理论有相当出色的表现。在测试的近百个困难欧氏几何定理中，三分之一以上只需要一项，只需要三四步简单操作就能够获证；绝大多数定理在两项之内可以完成证明，并通过减弱已知条件来加强定理结论的适用范围。本成果获得第32届国际符号和代数计算会议唯一的"杰出论文奖"。该奖由计算机科学协会(ACM)符号与代数计算专业委员会颁发。国际同行认为，该项工作是机器证明领域的一个突破，其意义超出该领域本身。