License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2013.335
URN: urn:nbn:de:0030-drops-40718
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4071/
Go to the corresponding LIPIcs Volume Portal

Winkler, Sarah ; Zankl, Harald ; Middeldorp, Aart

Beyond Peano Arithmetic – Automatically Proving Termination of the Goodstein Sequence

pdf-format:
24.pdf (0.5 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{winkler_et_al:LIPIcs:2013:4071,
  author =	{Sarah Winkler and Harald Zankl and Aart Middeldorp},
  title =	{{Beyond Peano Arithmetic – Automatically Proving Termination of the Goodstein Sequence}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{335--351},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{Femke van Raamsdonk},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4071},
  URN =		{urn:nbn:de:0030-drops-40718},
  doi =		{10.4230/LIPIcs.RTA.2013.335},
  annote =	{Keywords: term rewriting, termination, automation, ordinals}
}

Keywords: term rewriting, termination, automation, ordinals
Collection: 24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Issue Date: 2013
Date of publication: 24.06.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI