Ordinals in HOL: Transfinite arithmetic up to (and beyond) $\omega_1$

Authors

Michael Norrish and Brian Huffman

NICTA

Australian National University

Galois
Inc.

Abstract

We describe a comprehensive HOL mechanisation of the theory of ordinal numbers, focusing on the basic arithmetic operations. Mechanised results include the existence of fixpoints such as ε₀, the existence of normal forms, and the validation of some of the algorithms used in the ACL2 theorem-proving system.

BibTeX Entry

  @inproceedings{Norrish_Huffman_13,
publisher        = {Springer},
booktitle        = {International Conference on Interactive Theorem Proving},
month            = jul,
paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/6676.pdf},
slides           = {http://ts.data61.csiro.au/publications/nicta_slides/6676.pdf},
year             = {2013},
editor           = {{Sandrine Blazy and Christine Paulin-Mohring and David Pichardie}},
title            = {Ordinals in {HOL}: Transfinite Arithmetic up to (and beyond) $\omega_1$},
author           = {Norrish, Michael and Huffman, Brian},
}