Adding a Total Order to ACL2
Panagiotis Manolios and Matt Kaufmann.
The Third International Workshop on the ACL2 Theorem Prover, April 2002.
We show that adding a total order to ACL2, via new axioms, allows for
simpler and more elegant definitions of functions and libraries of
theorems. We motivate the need for a total order with a simple
example and explain how a total order can be used to simplify existing
libraries of theorems (i.e., ACL2 books) on finite set theory and
records. These ideas have been incorporated into ACL2 Version 2.6,
which includes axioms positing a total order on the ACL2 universe.
Gzipped Postscript (53K)