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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Castéran, P., Contejean, E.: On ordinal notations, http://coq.inria.fr/V8.2pl1/contribs/Cantor.html
Gordon, M.J.C., Reynolds, J., Hunt, Jr., W.A., Kaufmann, M.: An integration of HOL and ACL2. In: Proceedings of Formal Methods in Computer-Aided Design (FMCAD), pp. 153–160. IEEE Computer Society (2006)
Harrison, J.: The HOL wellorder library. HOL88 documentation (May 1992)
Huffman, B.: Countable ordinals. Archive of Formal Proofs, Formal proof development (November 2005), http://afp.sf.net/entries/Ordinal.shtml
Kaufmann, M., Slind, K.: Proof pearl: Wellfounded induction on the ordinals up to ε 0. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 294–301. Springer, Heidelberg (2007)
Manolios, P., Vroon, D.: Ordinal arithmetic: Algorithms and mechanization. Journal of Automated Reasoning 34(4), 387–423 (2005)
Traytel, D., Popescu, A., Blanchette, J.C.: Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, pp. 596–605. IEEE (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Norrish, M., Huffman, B. (2013). Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1 . In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds) Interactive Theorem Proving. ITP 2013. Lecture Notes in Computer Science, vol 7998. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39634-2_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-39634-2_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39633-5
Online ISBN: 978-3-642-39634-2
eBook Packages: Computer ScienceComputer Science (R0)