一句话：通过从希尔伯特第十问题归约，证明单规则重写系统线性解释终止性不可判定，并扩展至多种序与多项式解释。
本文研究重写系统终止性证明方法的可判定性边界。作者从希尔伯特第十问题出发构造简单归约，证明单规则重写系统在自然数上用线性解释可证终止这一问题是不可判定的；同一归约还推出使用带子项系数的 Knuth-Bendix 序时可证终止的不可判定性。进一步，论文表明即便单规则系统可由非线性多项式解释证明终止，线性终止问题仍不可判定，并证明用有理数或实数系数的多项式解释可证终止的问题也不可判定。若干结果已在 Isabelle/HOL 证明助手中形式化验证。
By means of a simple reduction from Hilbert's 10th problem we prove the somewhat surprising result that termination of one-rule rewrite systems by a linear interpretation in the natural numbers is undecidable. The very same reduction also shows the undecidability of termination of one-rule rewrite systems using the Knuth-Bendix order with subterm coefficients. The linear termination problem remains undecidable for one-rule rewrite systems that can be shown terminating by a (non-linear) polynomial interpretation. We further show the undecidability of the problem whether a one-rule rewrite system can be shown terminating by a polynomial interpretation with rational or real coefficients. Several of our results have been formally verified in the Isabelle/HOL proof assistant.