Skip navigation
Skip navigation

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

Norrish, Michael; Huffman, Brian

Description

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 ε 0, the existence of normal forms, and the validation of algorithm

CollectionsANU Research Publications
Date published: 2013
Type: Book chapter
URI: http://hdl.handle.net/1885/66272
DOI: 10.1007/978-3-642-39634-2_12

Download

File Description SizeFormat Image
01_Norrish_Ordinals_in_HOL:_Transfinite_2013.pdf2.26 MBAdobe PDF    Request a copy
02_Norrish_Ordinals_in_HOL:_Transfinite_2013.pdf264.82 kBAdobe PDF    Request a copy


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  20 July 2017/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator