A mechanizable first-order theory of ordinals

DOI10.1007/978-3-319-66902-1_20zbMATH Open1496.68371OpenAlexW2751733221MaRDI QIDQ1694476FDOQ1694476

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

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

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)

Cited In (8)

• Type-theoretic approaches to ordinals
• Formalizing calendars with the category of ordinals
• Formal Methods in Computer-Aided Design
• Two First-Order Theories of Ordinals
• Title not available (Why is that?)
• Ordinal arithmetic: Algorithms and mechanization
• Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)
• The theory of ordinal length

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)