线性程序的Ranking函数自动合成 (2009年)

针对判定一个程序终止性的经典方法Ranking函数法，运用半代数系统的概念，把程序终止性问题转换为求半代数系统的Rankin9函数。然后运用符号计算工具DISCOY-ERER和Farkas引理，求出函数参数存在的充分必要条件，并根据符号计算理论的方法自动合成Ranking函数。通过计算代数理论的证明和试验的验证，并与其他方法做了比较，这种方法是高效合理的。