线性终止问题在N上是不可判定的。
摘要：多项式解释在自然数中是否能够证明一个术语重写系统是终止的是不可判定的，最近已经有人证明了这一点。本文进一步证明，当将解释限制为线性多项式时（正如工具中经常做的那样），并且只考虑单规则重写系统时，这个情况仍然成立。更重要的是，新的不可判定性证明比以前的证明更简单。我们还进一步证明了有理数/实数上的多项式终止性是不可判定的。 标题翻译：多项式解释下的重写系统终止性的不可判定性
作者：Fabian Mitterwallner, Aart Middeldorp and Ren''e Thiemann
论文ID：2307.14805
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-28