Panagiotis (Pete) Manolios
College of Computer and Information Science
Northeastern University

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)