Panagiotis (Pete) Manolios
College of Computer and Information Science
Northeastern University

Algorithms for Ordinal Arithmetic

Panagiotis Manolios and Daron Vroon.
Nineteenth International Conference on Automated Deduction (CADE), pages 243-257. Springer-Verlag, July 2003. © Springer-Verlag.


Proofs of termination are essential for establishing the correct behavior of computing systems. There are various ways of establishing termination, but the most general involves the use of ordinals. An example of a theorem proving system in which ordinals are used to prove termination is ACL2. In ACL2, every function defined must be shown to terminate using the ordinals up to epsilon0. We use a compact notation for the ordinals up to epsilon0 (exponentially more succinct than the one used by ACL2) and define efficient algorithms for ordinal addition, subtraction, multiplication, and exponentiation. In this paper we describe our notation and algorithms, prove their correctness, and analyze their complexity.

Gzipped Postscript (87K) © Springer-Verlag.
PDF (233K) © Springer-Verlag.
Postscript (230K) © Springer-Verlag.