Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω1
Date
2013
Authors
Norrish, Michael
Huffman, Brian
Journal Title
Journal ISSN
Volume Title
Publisher
Springer Science + Business Media
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 ε 0, the existence of normal forms, and the validation of algorithm
Description
Keywords
Keywords: Arithmetic operations; Fixpoints; Mechanisation; Normal form; Ordinal number; Machinery; Number theory; Theorem proving
Citation
Collections
Source
Type
Book chapter
Book Title
Lecture Notes in Computer Science: Interactive Theorem Proving
Entity type
Access Statement
License Rights
Restricted until
2037-12-31