Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω1

Michael Norrish; Brian Huffman

doi:10.1007/978-3-642-39634-2_12

Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁

Michael Norrish, Brian Huffman

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

7 Citations (Scopus)

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 algorithms used in the ACL2 theorem-proving system.

Original language	English
Title of host publication	Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings
Pages	133-146
Number of pages	14
DOIs	https://doi.org/10.1007/978-3-642-39634-2_12
Publication status	Published - 2013
Event	4th International Conference on Interactive Theorem Proving, ITP 2013 - Rennes, France Duration: 22 Jul 2013 → 26 Jul 2013

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7998 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	4th International Conference on Interactive Theorem Proving, ITP 2013
Country/Territory	France
City	Rennes
Period	22/07/13 → 26/07/13

Access to Document

10.1007/978-3-642-39634-2_12

Cite this

Norrish, M., & Huffman, B. (2013). Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁. In Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings (pp. 133-146). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7998 LNCS). https://doi.org/10.1007/978-3-642-39634-2_12

@inproceedings{e4427791a23044faa14c13794f3c1c4c,

title = "Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω1",

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 algorithms used in the ACL2 theorem-proving system.",

author = "Michael Norrish and Brian Huffman",

year = "2013",

doi = "10.1007/978-3-642-39634-2_12",

language = "English",

isbn = "9783642396335",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "133--146",

booktitle = "Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings",

note = "4th International Conference on Interactive Theorem Proving, ITP 2013 ; Conference date: 22-07-2013 Through 26-07-2013",

}

Norrish, M & Huffman, B 2013, Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁. in Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7998 LNCS, pp. 133-146, 4th International Conference on Interactive Theorem Proving, ITP 2013, Rennes, France, 22/07/13. https://doi.org/10.1007/978-3-642-39634-2_12

Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁. / Norrish, Michael; Huffman, Brian.
Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings. 2013. p. 133-146 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7998 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Ordinals in HOL

T2 - 4th International Conference on Interactive Theorem Proving, ITP 2013

AU - Norrish, Michael

AU - Huffman, Brian

PY - 2013

Y1 - 2013

N2 - 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 algorithms used in the ACL2 theorem-proving system.

AB - 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 algorithms used in the ACL2 theorem-proving system.

UR - http://www.scopus.com/inward/record.url?scp=84882762773&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-39634-2_12

DO - 10.1007/978-3-642-39634-2_12

M3 - Conference contribution

SN - 9783642396335

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 133

EP - 146

BT - Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings

Y2 - 22 July 2013 through 26 July 2013

ER -