Ordinals in HOL: Transfinite Arithmetic up to (and beyond) ω?

Select |




Print


Norrish, Michael; Huffman, Brian

Norrish, Michael; Huffman, Brian


2013-07-22


Conference Material


Interactive Theorem Proving (ITP)


Rennes, France


133-146


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.


Springer


http://itp2013.inria.fr/


nicta:6676


Norrish, Michael; Huffman, Brian. Ordinals in HOL: Transfinite Arithmetic up to (and beyond) ω?. In: Sandrine Blazy and Christine Paulin-Mohring and David Pichardie Editor, editor/s. Interactive Theorem Proving (ITP); Rennes, France. Springer; 2013-07-22. 133-146.



Loading citation data...

Citation counts
(Requires subscription to view)