从有理数域上的矩阵解释到自然数域上的矩阵解释
摘要：矩阵解释广义化了线性多项式解释，并已被证明在自动证明术语重写系统终止的工具实现中是有用的。考虑到有理系数在多项式解释中的成功应用，我们最近将传统的矩阵解释（在矩阵条目中使用自然数）推广到包含实数的情况。然而，现有的结果无法将形式上证明实数多项式比自然数多项式在证明重写系统终止时更强大的结论推广到矩阵解释中。在本文中，我们对这个问题进行了更深入的研究。我们展示了在一些条件下，可以将满足一组符号约束的有理数矩阵解释转化为满足约束的自然数矩阵解释（使用更大的矩阵）。
作者：Salvador Lucas
论文ID：1007.0143
分类：Symbolic Computation
分类简称：cs.SC
提交时间：2010-07-02