manolios@cc.gatech.edu
College of Computing
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).
|
Last modified: Mon Jun 21 10:55:06 EDT 2004
manolios@cc.gatech.edu |
College of Computing |