一类Riemann张量指标表达式的标准型完全分类及其在微分几何中的应用

本文研究了n维微分几何中Riemann张量指标表达式的标准型完全分类问题, 通过引入指标结构图的概念, 证明了规范类型单项式都是标准型, 并且构成次数不大于5 的Sakai类型单项式的正交基底, 由此得到Sakai类型单项式的标准型完全分类, 这是次数大于3时标准型完全分类问题的第一个结果. 同时给出了相应标准化算法, 通过比较说明了该算法比现有算法更加简便, 最后应用于自动推导和证明微分几何中关于Riemann张量的一些公式.     

基于指标形式张量的微分几何定理机器证明

提出了一个基于指标形式张量的微分几何定理的机器证明算法.该算法将微分几何定理转化成带指标的张量多项式的计算问题,然后通过利用重写规则,挖掘等价条件和分次选取条件等方法大大减少了这个多项式系统的方程个数.再利用这个多项式系统本身和关于哑元的方程三角化这个多项式系统,将所得到的首项代入结论, 从而得到了该定理的机器证明.该算法不仅能够证明基于指标形式张量的微分几何定理,也可以用于张量方程的求解.