从2014年到2017年，先进制造部邵长鹏等科研人员在符号计算研究方面陆续取得了如下五个方面的成果。

一、经典不变量理论的不变除法和拉直算法问题

括号代数是研究经典不变量理论的基本代数结构。括号代数的研究有着很长的历史，可以追溯到1845年，由Cayley首次建立，后来经Klein和Hilbert等数学家发展成熟。近代，随着计算机的发展，不变量理论的符号处理方法在Rota及其学派的工作下得到了新的发展。不变量理论在计算机视觉、机器人、自动推理,等领域都有着重要应用。虽然不变量的应用很广泛，但其基本代数算法的效率并不高，最典型两个问题是除法问题和拉直算法问题。

对于除法问题，在2014年，他们首次找到了括号代数中的一个可允许序，并建立了括号代数上的不变除法理论，同时也建立了括号代数上的不变Groebner基理论。这种不变除法的意义主要体现在和坐标多项式除法的比较上：虽然坐标多项式的除法和因式分解可用来做几何定理证明。但是在几何定理的发现上，这种运算往往缺乏几何意义。在射影几何中，虽然不变除法可以处理的问题不比坐标多项式多，但是这种不变除法更适合处理几何计算，因为这种运算的结果都具有几何意义。

括号代数中的不变除法和不变Groebner基理论背后的计算都依赖于拉直算法，目前已有的拉直算法包括：Young拉直算法（1928年）、Rota拉直算法（1978年）和White拉直算法（1991年）。其中Rota拉直算法的效率最高。但是Rota拉直算法有一个缺陷：虽然每一步的计算都很简单，但是需要计算的量随着次数和维数的增加呈现出指数型增长，这使得Rota拉直算法的效率会越来越低。

2015-2016年，他们提出了对偶括号的概念，依此建立了括号代数中一个新的拉直算法。相对于Rota拉直算法，他们提出的拉直算法的计算量不是很大，每一步计算的消耗可能会比Rota拉直算法多，但是平均之后整体的效率远远超过Rota拉直算法，下面是一些例子的时间统计结果，这些例子可以表现出算法效率的提高是很大的。目前，他们正在试图改进这一新的拉直算法中每一步计算的效率。

 

二、几何定理自动证明

自吴方法的提出，随后Groebner基，向量代数方法等陆续在几何定理自动证明中发挥重要作用。2015年的3月至7月，他们通过研究奥林匹克207个立体几何问题，试图比较这些经典方法的效率。他们的贡献不仅仅是提供一些具有代表性的机器证明的例子，可以用来区分这些方法的效率，最重要的是：对吴方法的非退化条件的选取做出了改进。

如果按照吴先生的定义，非退化条件是初式，但是他们发现这样选取非退化条件并不合适，而是需要从错误的分支里挑选，也即，这个非退化条件能够排除掉所有错误的分支，与此同时尽可能多地保留正确分支。

另外这一工作也促使他们考虑关于机器证明的其他问题，下面列举两个代表性的问题：

（1）如何在这些错误的分支里选取好的非退化条件？

（2）吴方法和Groebner基的非退化条件的等价性问题。虽然Groebner基是一个完全性的自动证明方法，但是Groebner基的非退化条件的选取显得更加困难。原因在于，这个方法首先求出假定条件生成的理想I的理想的Groebner基G1，然后还需要求出I相对于结论的饱和理想J的Groebner基G2。按照Groebner基的想法，非退化条件的集合为J\I，而计算中通常是从G2\G1里选取，如果Groebner基的元素很复杂的话，那这些非退化条件就很难解释。在很多情况下，吴方法得到的非退化条件（吴先生的定义）是落在J\I里，而不在G2\G1里。如果换成现在的定义，则这两个方法得到的非退化条件是否等价？

三、四元数方程求解

研究这个问题的初衷是希望解决实际中和旋转、平移有关的多元二次方程组问题。四元数可以表示三维旋转，且比SO(3)表示旋转更加简洁有效，所以在实际问题中遇到和旋转有关的问题都可以用四元数来表示。一般而言，在求解这类方程的时候往往都是把四元数写成分量形式，把问题转变成常见的多元二次方程组问题。因此，如果存在直接解决四元数方程的方法，则对于解决这类问题会有很大的帮助。

然而，这个问题是非常困难的。首先，代数基本定理在四元数上是不成立的。1944年，Eilenberg 和Niven给出一个四元数斜域上的弱的代数基本定理。其次，线性四元数方程式作为最简单的一类方程，并没有直接在四元数框架下求解的方法。目前比较好的结果是2013年Schwartz的结果，这是对1884年Sylvester解法的一个推广。

他们的主要工作是针对线性四元数方程的直接求解办法。Schwartz的想法已经不能再做推广，我们以Grassmann代数为工具，给出了一般情形的线性四元数解的具体表达式。结果表明最终的解，可以简单地通过左右乘以若干已知四元数得到。在2016年，又通过四维Clifford代数对这一求解方法给出了更加简明的解释。他们的下一步目标是解决二次四元数方程。

四、线几何与几何代数

几何代数是四元数的高维推广，是一种代数运算具有几何意义的代数工具。线几何是研究R4中直线的学科，也就是三维射影空间P3。经过Pluecker变换，线几何与R3,3之间有着天然的联系，从而可以通过R3,3模型来研究线几何。但是，P3和R3,3之间关系的代数理论不是完善的，这是由于Pluecker变换不满射导致的，而且行列式为负数的射影变换在Pluecker变换下并不能诱导R3,3中的正交变换。从这一问题出发，他们陆续得到了下面的结论：

（1）采用了两种不同的方法（一个是矩阵的方法，一个是几何代数的方法）给出了Pluecker变换逆映射的完全表达形式。对于Pluecker变换的不足之处，将群SO(3,3)扩大成更一般的群RL(3,3)，从而使得点到点的射影变换、点到面的射影变换和RL(3,3)单位处的连通分支建立一一对应关系。进而完善了三维射影变换和三维对偶射影变换与六维正交变换和六维反正交变换之间的对应关系，并给出了这种对应关系的协变性。

（2）发现了3维反射和刚体运动在spinor表示下的完全分解形式。作为这种分解的一个推论表明：刚体变换可以分解成两个180度角的三维旋转的复合。除此之外，还建立了刚体变换群的李代数se(3)的螺旋表示的差积运算与虚功之间的关系。

（3）把刚体变换群的李代数se(3)的螺旋表示的差积运算与虚功理论推广到更一般的sl(4) 的六维李子代数，并建立了超螺旋理论。

这一工作发表在第6届几何代数在计算机科学和工业中的应用会议 (AGACSE’15) 上，并获得了首届David Hestense奖。该奖是几何代数领域首次设立的奖项。这篇文章获得了最佳论文奖，在62篇论文中排名第一。

五、平底刀高阶切触的残留高度公式

这是数控加工中的一个问题，问题的叙述是：给了一个曲面，用一个底部是平面圆盘的刀片从上面划过去，再划回来。这两个圆柱槽相交之后，残留下来中间的部分与指定的目标曲面的距离称为残留高度。在低阶切触情形下，残留高度有经典的表达式；但是在高阶切触的情形，缺乏相应的结果。提高切触的阶数对于大幅度降低加工轨道的长度影响极大。我们对于各种高阶切触的情形，推导出了相关的残留高度表达式，并通过实物加工验证了相对于低阶切触的明显改进。这一工作在SIAM 2015分会上做过口头报告。