微分差分多项式系统高效消元算法研究

消元理论与算法是数学机械化的核心研究内容，特征列方法与结式方法是其中两个基本消元算法。目前代数方程与微分方程的特征列与代数方程的结式方法已经相当成熟并得到广泛应用，而差分方程的特征列与微分方程的结式方法研究才刚刚起步。我们建立了常差分与常微分-差分混合系统的特征列方法，给出了微分Chow形式与微分结式的相关理论与算法。本项目将在我们已有工作的基础上，进一步研究偏差分方程组的特征列方法及微分方程组的结式方法及其应用，研究内容包括：在特征列方法方面，发展偏差分核理论，研究偏差分升列的性质，解决偏差分情形下的根理想成员判定问题，并将这些结果应用于偏差分情形的定理机器证明；在微分结式方面，研究微分结式的矩阵表示以及微分sparse结式次数界问题；在算法设计方面，研究微分结式、微分sparse结式与微分Chow形式的高效符号算法及其应用。

本项目主要研究了稀疏微分与差分结式的基本性质与计算问题。给出了稀疏微分（差分）结式存在的充分必要条件，证明了稀疏微分（差分）结式具有类似于代数结式的性质，并以此为基础给出了计算稀疏微分（差分）结式的单指数算法。此外，结式的矩阵表示可以极大地简化结式的表达与计算，我们针对两个任意次数的一阶单变元微分多项式的结式的矩阵表示问题，证明了基于我们方法构作的矩阵是非奇异的，微分结式则是所构作矩阵行列式的非零因子。这是首个针对一类非线性微分多项式给出的矩阵表示。