Ordinal Arithmetic in ACL2
Panagiotis Manolios and Daron Vroon.
Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2003), July 2003.
Abstract
Ordinals form the basis for termination proofs in ACL2.
Currently, ACL2 uses a rather inefficient representation for
the ordinals up to epsilon0 and provides limited support
for reasoning about them. We present algorithms for ordinal
arithmetic on an exponentially more compact representation than
the one used by ACL2. The algorithms have been
implemented and numerous properties of the arithmetic operators
have been mechanically verified, thereby greatly extending
ACL2's ability to reason about the ordinals. We describe how
to use the libraries containing these results, which are
currently distributed with ACL2 version 2.7.
Gzipped Postscript (81K).
PDF (210K).
Postscript (208K).