Sciweavers

Share
CADE
2003
Springer

Algorithms for Ordinal Arithmetic

9 years 8 months ago
Algorithms for Ordinal Arithmetic
Ordinals form the basis for termination proofs in ACL2. Currently, ACL2 uses a rather inefficient representation for the ordinals up to 0 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.
Panagiotis Manolios, Daron Vroon
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2003
Where CADE
Authors Panagiotis Manolios, Daron Vroon
Comments (0)
books