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.

• Type: Conference
• Year: 2003
• Where: CADE
• Authors: Panagiotis Manolios, Daron Vroon
• Keywords: Automated Reasoning, CADE 2003, Limited Support, Numerous Properties, Termination Proofs