Extensions of arithmetic for proving termination of computations

DOI10.2307/2274742MaRDI QIDQ4732468zbMATH OpenOpenAlexFDO

Authors Clement F. Kent, Bernard Hodgson

Publication date 1989

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2307/2274742

zbMATH Keywords

\(\Sigma\)- reflectionGoodstein predecessorGoodstein sequenceprovable ordinalsprovably recursive function

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30)

Recommendations

• Beyond Peano arithmetic -- automatically proving termination of the Goodstein sequence
• Predicatively unprovable termination of the Ackermannian Goodstein process
• Goodstein's function
• Goodstein sequences for prominent ordinals up to the Bachmann-Howard ordinal
• scientific article; zbMATH DE number 1215495

Cites work

• Accessible Independence Results for Peano Arithmetic
• scientific article; zbMATH DE number 3686772 (Why is no real title available?)
• scientific article; zbMATH DE number 3550181 (Why is no real title available?)
• Proving termination with multiset orderings
• Termination of rewriting

Cited in

(10)

• Termination of rewriting
• Analytic combinatorics, proof-theoretic ordinals, and phase transitions for independence results
• Beyond Peano arithmetic -- automatically proving termination of the Goodstein sequence
• On the Computational Content of Termination Proofs
• Goodstein's function
• scientific article; zbMATH DE number 5693751 (Why is no real title available?)
• scientific article; zbMATH DE number 88985 (Why is no real title available?)
• Goodstein sequences for prominent ordinals up to the Bachmann-Howard ordinal
• Goodstein's theorem revisited
• A survey of ordinal interpretations of type ɛ0 for termination of rewriting systems

This page was built for publication: Extensions of arithmetic for proving termination of computations

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