Abstract: 

In termination analysis of term rewrite systems one of the oldest techniques uses polynomial interpretations over the natural numbers. While many other related techniques have been proven to be undecidable over the years, this was unknown for polynomial termination. It has been conjectured to be undecidable in the literature, but we only recently found a proof confirming the conjecture.

We showed the result via a reduction from Hilbert's 10th problem. Additionally we could prove that related and more restricted properties like incremental polynomial termination, polynomial termination over the real and ration numbers, and linear polynomial termination are also undecidable.

In this talk I will discuss the technique of polynomial termination itself, as well as explain the rough structure and idea behind the undecidability proof.