Adding a Total Order to ACL2

Panagiotis Manolios and Matt Kaufmann.
The Third International Workshop on the ACL2 Theorem Prover, April 2002.

Abstract

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)
PDF (139K)
Postscript (132K)

Last modified: Mon Jun 21 10:55:33 EDT 2004
manolios@cc.gatech.edu

Back to Pete's home page
College of Computing