2026-07-21T19:26:09Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4071 2024-03-06T10:34:47Z ddc:004 open_access

Beyond Peano Arithmetic – Automatically Proving Termination of the Goodstein Sequence Winkler, Sarah Zankl, Harald Middeldorp, Aart term rewriting termination automation ordinals Kirby and Paris (1982) proved in a celebrated paper that a theorem of Goodstein (1944) cannot be established in Peano (1889) arithmetic. We present an encoding of Goodstein's theorem as a termination problem of a finite rewrite system. Using a novel implementation of ordinal interpretations, we are able to automatically prove termination of this system, resulting in the first automatic termination proof for a system whose derivational complexity is not multiple recursive. Our method can also cope with the encoding by Touzet (1998) of the battle of Hercules and Hydra, yet another system which has been out of reach for automated tools, until now. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sarah Winkler and Harald Zankl and Aart Middeldorp 2013 Is Part Of LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2013.335 urn:nbn:de:0030-drops-40718 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.335 eng https://creativecommons.org/licenses/by/3.0/legalcode