|
|||||
|
|
| 几何代数在定理证明中的消元与化简算法 | |
| 引用本文： | 曹源昊,李洪波. 几何代数在定理证明中的消元与化简算法[J]. 系统科学与数学, 2009, 29(9): 1189-1199 |
| 作者姓名： | 曹源昊 李洪波 |
| 作者单位： | 中国科学院数学机械化中心,北京,100190 |
| 基金项目： | 国家自然科学基金NSFC，国家重点基础性研究基金NKBRSF |
| 摘 要： | 在符号计算中,最困难的一个地方是中间计算过程的表达式快速膨胀.基于不变量代数的符号几何计算为解决这个困难提供了可能.比如,利用零几何代数证明欧氏几何定理时,就可以给出很短的证明,甚至是单项式证明.中间的证明过程里有很多地方涉及到消元,展开,化简等问题.从程序实现的角度出发,在充分利用零几何代数计算特点的基础上,给出用于机器证明的消元、化简算法. |
| 关 键 词： | 共形几何代数 零括号代数 几何自动推理 算法. |
| 收稿时间： | 2009-06-30 |
ALGORITHMS OF ELIMINATION AND SIMPLIFICATION BASED ON GEOMETRIC ALGEBRA IN AUTOMATIC PROVING OF GEOMETRIC THEOREM |
|
| CAO Yuanhao,LI Hongbo. ALGORITHMS OF ELIMINATION AND SIMPLIFICATION BASED ON GEOMETRIC ALGEBRA IN AUTOMATIC PROVING OF GEOMETRIC THEOREM[J]. Journal of Systems Science and Mathematical Sciences, 2009, 29(9): 1189-1199 | |
| Authors: | CAO Yuanhao LI Hongbo |
| Affiliation: | Key Laboratory of Mathematics Mechanization, Chinese Academy of Sciences, Beijing 100090 |
| Abstract: | 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. |
| Keywords: | Conformal geometric algebra null bracket algebra automated geometry reasoning algorithm. |
| 本文献已被 万方数据 等数据库收录！ | |
| 点击此处可从《系统科学与数学》浏览原始摘要信息 | |
| 点击此处可从《系统科学与数学》下载全文 | |