A mechanizable first-order theory of ordinals

DOI10.1007/978-3-319-66902-1_20MaRDI QIDQ1694476zbMATH OpenOpenAlexFDO

Authors Peter H. Schmitt

Publication date 2 February 2018

Full work available at URL https://doi.org/10.1007/978-3-319-66902-1_20

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Ordinal arithmetic: Algorithms and mechanization
• Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)
• Algorithms for ordinal arithmetic.
• On computer-assisted proofs in ordinal number theory
• Beyond Peano arithmetic -- automatically proving termination of the Goodstein sequence

Cited in

(8)

• The theory of ordinal length
• Type-theoretic approaches to ordinals
• Formalizing calendars with the category of ordinals
• Formal Methods in Computer-Aided Design
• Two First-Order Theories of Ordinals
• scientific article; zbMATH DE number 7204430 (Why is no real title available?)
• Ordinal arithmetic: Algorithms and mechanization
• Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)

This page was built for publication: A mechanizable first-order theory of ordinals

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