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

Ordinal Arithmetic in ACL2

Panagiotis Manolios and Daron Vroon.
Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2003), July 2003.


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).