Algorithms for Ordinal Arithmetic

11 years 6 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)