Beyond Peano arithmetic -- automatically proving termination of the Goodstein sequence

DOI10.4230/LIPICS.RTA.2013.335MaRDI QIDQ2958394zbMATH OpenOpenAlexFDO

Authors Sarah Winkler, Harald Zankl, Aart Middeldorp

Publication date 1 February 2017

Full work available at URL https://doi.org/10.4230/LIPIcs.RTA.2013.335

zbMATH Keywords

automationordinalsterm rewritingtermination

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Recommendations

• Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations
• On some slowly terminating term rewriting systems
• Extensions of arithmetic for proving termination of computations
• Predicatively unprovable termination of the Ackermannian Goodstein process
• A new proof-theoretic proof of the independence of Kirby-Paris' hydra theorem.

Cited in

(6)

• A new proof-theoretic proof of the independence of Kirby-Paris' hydra theorem.
• A mechanizable first-order theory of ordinals
• On some slowly terminating term rewriting systems
• Extensions of arithmetic for proving termination of computations
• Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations
• Goodstein's theorem revisited

This page was built for publication: Beyond Peano arithmetic -- automatically proving termination of the Goodstein sequence

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2958394)