Ordinals in HOL: transfinite arithmetic up to (and beyond) _1

DOI10.1007/978-3-642-39634-2_12MaRDI QIDQ5327341zbMATH OpenOpenAlexFDO

Authors Michael Norrish, Brian Huffman

Publication date 7 August 2013

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-39634-2_12

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Ordinal and cardinal numbers (03E10)

Recommendations

• Ordinal arithmetic: Algorithms and mechanization
• A mechanizable first-order theory of ordinals
• Algorithms for ordinal arithmetic.
• Proof Pearl: Wellfounded Induction on the Ordinals Up to ε 0
• Cardinals in Isabelle/HOL

Cited in

(11)

• A mechanizable first-order theory of ordinals
• Unique solutions of contractions, CCS, and their HOL formalisation
• Cardinals in Isabelle/HOL
• Proof-producing reflection for HOL. With an application to model polymorphism
• Unique solutions of contractions, CCS, and their HOL formalisation
• Cofinality changes required for a large set of unapproachable ordinals below $\aleph _{\omega +1}$
• Formalizing ordinal partition relations using Isabelle/HOL
• scientific article; zbMATH DE number 7204430 (Why is no real title available?)
• Formal Methods in Computer-Aided Design
• Algorithms for ordinal arithmetic.
• Ordinal arithmetic: Algorithms and mechanization

Describes a project that uses

Uses Software

• ACL2
• HOL

This page was built for publication: Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)

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