首页    期刊浏览 2024年11月14日 星期四
登录注册

文章基本信息

  • 标题:Beyond Peano Arithmetic - Automatically Proving Termination of the Goodstein Sequence
  • 本地全文:下载
  • 作者:Sarah Winkler ; Harald Zankl ; Aart Middeldorp
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2013
  • 卷号:21
  • 页码:335-351
  • DOI:10.4230/LIPIcs.RTA.2013.335
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要: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.
  • 关键词:term rewriting; termination; automation; ordinals
国家哲学社会科学文献中心版权所有