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

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

MECHANICAL THEOREM PROVING FOR TENSOR WITH INDEXES IN DIFFERENTIAL GEOMETRY

A method for mechanically proving theorems for tensor with indexes in differential geometry is presented. The theorem is firstly converted into the problem of solving polynomial equations with indexes. To reduce the complexity of computation, various methods are proposed, including using rewriting rules, choosing tensor equations group by group, etc. Then the polynomial equations are triangulatd, taking the advantage of dummy indexes of the system. With theresults of the triangulation, the proof of the theorem is obtained. This method can not only prove theorems for tensor with indexes, but can also be used for tensor calculation.