Goodstein sequences and theorems are very popular because of their unboundedness with respect to multiple recursive functions and derivational complexity.

Showing the termination of Goodstein sequences and showing this termination automatically are both research topics that call for algebraic expertise. The authors encode Goodstein’s result as a termination problem of a finite rewrite system.

The authors use ordinal interpretations in implementing algebras to automatically show the termination of a system. They present 13 definitions, seven theorems, seven lemmas, and 20 examples in support of their method. The authors claim that their method is the first of its kind to automatically show the termination of a “system whose derivational complexity is not multiple recursive.”

For the implementation of their method, the authors combine ordinal algebras with matrix interpretations for the automatic termination proof. They further find that it manages Goodstein sequences within nine seconds, where a problem has approximately 120,000 variables and 300,000 clauses. The authors experiment on 1,463 termination tools for rewriting systems in the standard category of the termination problems database (TPDB). In the future, they propose the use of termination tools for rewrite systems with high derivational complexity.

The authors’ ideas of automating elementary interpretations for termination analysis make this paper an interesting read. They further claim that their method can automatically prove termination of two specific systems, namely, the battle of Hercules and Hydra, and the Worm battle.