Ordinals in HOL: Transfinite arithmetic up to (and beyond) $\omega_1$
Authors
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}, address = {Rennes, France}, pages = {133--146} }