Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1

DOI10.1007/978-3-642-39634-2_12zbMath1317.68227OpenAlexW1604540818MaRDI QIDQ5327341

Brian Huffman, Michael Norrish

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)

Related Items (4)

Proof-Producing Reflection for HOL ⋮ Unnamed Item ⋮ Unique solutions of contractions, CCS, and their HOL formalisation ⋮ Unnamed Item

Uses Software

• ACL2
• HOL

This page was built for publication: Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1