Beyond Polynomials and Peano Arithmetic – Automation of Elementary and Ordinal Interpretations

Harald Zankl, Sarah Winkler, and Aart Middeldorp

Journal of Symbolic Computation 69, pp. 129 – 158, 2015.


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 algebras based on 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 as well as a (corrected) encoding by Beklemishev (2006) of the Worm battle, two further systems which have been out of reach for automatic tools, until now. Based on our ideas of implementing ordinal algebras we also present a new approach for the automation of elementary interpretations for termination analysis.


  PDF |    doi:10.1016/j.jsc.2014.09.033  |   © 2014 Elsevier Ltd.


author = "Harald Zankl and Sarah Winkler and Aart Middeldorp",
title = "Beyond Polynomials and {P}eano Arithmetic -- Automation of
Elementary and Ordinal Interpretations",
journal = "Journal of Symbolic Computation",
volume = 69,
pages = "129--158",
year = 2015,
doi = "110.1016/j.jsc.2014.09.033"
Nach oben scrollen