Ordinal Arithmetic: Algorithms and Mechanization
Panagiotis Manolios and Daron Vroon.
Journal of Automated Reasoning, to appear. © Springer-Verlag.
Termination proofs are of critical importance for establishing the correct behavior of both transformational and reactive computing systems. A general setting for establishing termination proofs involves the use of the ordinal numbers, an extension of the natural numbers into the transfinite which were introduced by Cantor in the nineteenth century and are at the core of modern set theory. We present the first comprehensive treatment of ordinal arithmetic on compact ordinal notations and give efficient algorithms for various operations, including addition, subtraction, multiplication, and exponentiation.
Using the ACL2 theorem proving system, we implemented our
ordinal arithmetic algorithms, mechanically verified their
correctness, and developed a library of theorems that can be
used to significantly automate reasoning involving the
ordinals. To enable users of the ACL2 system to fully utilize
our work required that we modify ACL2, e.g., we replaced the
underlying representation of the ordinals and added a large library
of definitions and theorems. Our modifications are available
starting with ACL2 version 2.8.
PDF (319K) © Springer-Verlag.
Gzipped Postscript (177K) © Springer-Verlag.
Postscript (1012K) © Springer-Verlag.