**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### Abstract

We formalize several undecidability results on termination
for

*one-rule*term rewrite systems by means of simple reductions from Hilbert's 10th problem. To be more precise, for a class \(C\) of reduction orders, we consider the question for a given rewrite rule \(\ell \to r\), whether there is some reduction order \({\succ} \in C\) such that \(\ell \succ r\). We include undecidability results for each of the following classes \(C\):- the class of
*linear*polynomial interpretations over the natural numbers, - the class of linear polynomial interpretations over
the natural numbers in the
*weakly monotone*setting, - the class of Knuth–Bendix orders with
*subterm coefficients*, - the class of
*non-linear*polynomial interpretations over the natural numbers, and - the class of non-linear polynomial interpretations over the
*rational*and*real*numbers.

### License

### Topics

### Related publications

- Mitterwallner, F., Middeldorp, A., & Thiemann, R. (2024). Linear Termination is Undecidable. Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, 11, 1–12. https://doi.org/10.1145/3661814.3662081