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